--- a/src/Sequents/ILL/ILL_predlog.ML Thu Jun 16 20:30:37 2005 +0200
+++ b/src/Sequents/ILL/ILL_predlog.ML Fri Jun 17 11:34:04 2005 +0200
@@ -1,6 +1,3 @@
-
-open ILL_predlog;
-
fun auto1 x = prove_goal thy x
(fn prems => [best_tac safe_cs 1]) ;
--- a/src/Sequents/ILL/washing.ML Thu Jun 16 20:30:37 2005 +0200
+++ b/src/Sequents/ILL/washing.ML Fri Jun 17 11:34:04 2005 +0200
@@ -1,6 +1,3 @@
-
-open washing;
-
(* "activate" definitions for use in proof *)
val changeI = [context1] RL ([change] RLN (2,[cut]));