--- a/src/HOL/Modelcheck/MuckeExample2.ML Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: HOL/Modelcheck/MuckeExample2.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-
-(* prints the mucke output on the screen *)
-(* trace_mc := true; *)
-val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
-
-Goal "Reach2 True";
-by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
-by (mc_mucke_tac [] 1);
-qed "Reach_thm";
-
-(*alternative:*)
-goal thy "Reach2 True";
-by (mc_mucke_tac Reach_rws 1);
-qed "Reach_thm'";