# 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