src/HOL/Modelcheck/Example.ML

--- a/src/HOL/Modelcheck/Example.ML	Mon May 19 15:22:41 1997 +0200
+++ b/src/HOL/Modelcheck/Example.ML	Tue May 20 10:28:19 1997 +0200
@@ -13,8 +13,10 @@
 (*show the current proof state using the model checker syntax*)
 setmp print_mode ["Eindhoven"] pr ();
 
-(*actually invoke the model checker*)
-by (mc_tac 1);
+(* actually invoke the model checker *)
+(* try out after installing the model checker: see the README file *)
+
+(* by (mc_tac 1); *)
 
 (*qed "reach_ex_thm1";*)