File State.ML

Goal "empty({}:=Some {}) : {(e::State ~=> State). dom e = Pow {b. {b} \<in> dom e} &( ! s:dom e. the (e s) <= s) & (! s: dom(e). e(s) =  Some {b. b:s & (e({b}) = Some {b})})}";
by (simp_tac (simpset() addsimps [dom_def,empty_def]) 1);
qed "Exec_witness";