# HG changeset patch # User mueller # Date 863791819 -7200 # Node ID 9854e3ea09e7ac2f43038dd0e860c476ebdf95ca # Parent 44f01b718eab2281e2d2b8e52f45c20d2f76a0e9 commented out qed (in case the MC is unavailable); diff -r 44f01b718eab -r 9854e3ea09e7 src/HOL/Modelcheck/Example.ML --- 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";*) -