--- a/src/ZF/mono.ML Wed Apr 23 10:49:01 1997 +0200
+++ b/src/ZF/mono.ML Wed Apr 23 10:52:49 1997 +0200
@@ -180,13 +180,13 @@
val [PQimp] = goal IFOL.thy
"[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
by IntPr.safe_tac;
-be (PQimp RS mp RS exI) 1;
+by (etac (PQimp RS mp RS exI) 1);
qed "ex_mono";
val [PQimp] = goal IFOL.thy
"[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
by IntPr.safe_tac;
-be (spec RS (PQimp RS mp)) 1;
+by (etac (spec RS (PQimp RS mp)) 1);
qed "all_mono";
(*Used in intr_elim.ML and in individual datatype definitions*)