src/HOL/Modelcheck/Example.ML
changeset 3210 e80db1660614
child 3219 9854e3ea09e7
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/Example.ML	Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Modelcheck/Example.ML
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+val reach_rws = [reach_def,INIT_def,N_def];
+
+
+goal thy "reach (True,True,True)";
+by (simp_tac (MC_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*)
+by (mc_tac 1);
+
+qed "reach_ex_thm1";
+
+
+
+