--- a/src/HOL/Modelcheck/Example.ML Fri May 16 16:08:38 1997 +0200
+++ b/src/HOL/Modelcheck/Example.ML Fri May 16 16:10:19 1997 +0200
@@ -16,8 +16,7 @@
(*actually invoke the model checker*)
by (mc_tac 1);
-qed "reach_ex_thm1";
+(*qed "reach_ex_thm1";*)
-