--- a/src/HOL/Induct/LFilter.ML Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/LFilter.ML Fri Jul 31 10:48:42 1998 +0200
@@ -7,9 +7,6 @@
--defined by a combination of induction and coinduction
*)
-open LFilter;
-
-
(*** findRel: basic laws ****)
val findRel_LConsE =