src/HOL/Modelcheck/Example.ML
changeset 3380 2986e3b1f86a
parent 3225 cee363fc07d7
child 5069 3ea049f7979d
--- a/src/HOL/Modelcheck/Example.ML	Fri May 30 15:55:27 1997 +0200
+++ b/src/HOL/Modelcheck/Example.ML	Fri May 30 16:37:20 1997 +0200
@@ -18,7 +18,11 @@
 
 (* by (mc_tac 1); *)
 
-(*qed "reach_ex_thm1";*)
+(*qed "reach_ex_thm";*)
 
 
 
+(* just to make a proof in this file :-) *)
+goalw thy [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
+by (Simp_tac 1);
+qed"init_state";