--- a/src/HOL/UNITY/Reach.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Fri Jul 31 18:46:55 1998 +0200
@@ -7,8 +7,6 @@
[ this example took only four days!]
*)
-open Reach;
-
(*TO SIMPDATA.ML?? FOR CLASET?? *)
val major::prems = goal thy
"[| if P then Q else R; \