src/HOL/Modelcheck/MuckeExample2.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/MuckeExample2.ML	Thu Apr 22 10:56:37 1999 +0200
@@ -0,0 +1,28 @@
+(*  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 thy "Reach2 True";
+by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
+by (mc_mucke_tac thy [] 1);
+qed "Reach_thm";
+
+(* Alternative: *)
+goal thy "Reach2 True";
+by (mc_mucke_tac thy Reach_rws 1);
+qed "Reach_thm";
+
+
+*)
+
+
+