--- 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";
--- a/src/HOL/Modelcheck/Example.thy Fri May 30 15:55:27 1997 +0200
+++ b/src/HOL/Modelcheck/Example.thy Fri May 30 16:37:20 1997 +0200
@@ -4,7 +4,7 @@
Copyright 1997 TU Muenchen
*)
-Example = MCSyn +
+Example = CTL + MCSyn +
types