| 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";