# HG changeset patch
# User mueller
# Date 865003040 -7200
# Node ID 2986e3b1f86a4aae265eb7a237b2dde362345403
# Parent  7091ffa99c93ff088a2fbb5d451cff6987bee531
trivial changes to incorporate CTL.thy and Example.ML in html file;

diff -r 7091ffa99c93 -r 2986e3b1f86a src/HOL/Modelcheck/Example.ML
--- 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";
diff -r 7091ffa99c93 -r 2986e3b1f86a src/HOL/Modelcheck/Example.thy
--- 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