--- a/src/HOL/Modelcheck/EindhovenExample.ML Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Modelcheck/EindhovenExample.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-val reach_rws = [reach_def,INIT_def,N_def];
-
-
-Goal "reach (True,True,True)";
-by (simp_tac (Eindhoven_ss addsimps reach_rws) 1);
-
-(*show the current proof state using the model checker syntax*)
-setmp print_mode ["Eindhoven"] pr ();
-
-(* actually invoke the model checker *)
-(* try out after installing the model checker: see the README file *)
-
-(* by (mc_eindhoven_tac 1); *)
-
-(*qed "reach_ex_thm";*)
-
-
-
-(* just to make a proof in this file :-) *)
-Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
-by (Simp_tac 1);
-qed"init_state";