src/HOL/UNITY/Reach.ML
changeset 5232 e5a7cdd07ea5
parent 5196 1dd4ec921f71
child 5240 bbcd79ef7cf2
--- 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;    \