--- a/src/HOL/Induct/PropLog.ML Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Induct/PropLog.ML Fri Jul 31 10:48:42 1998 +0200
@@ -8,8 +8,6 @@
Prove: If H|=p then G|=p where G:Fin(H)
*)
-open PropLog;
-
(** Monotonicity **)
Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
by (rtac lfp_mono 1);