Conducted the IFOL proofs using intuitionistic tools

--- a/src/ZF/mono.ML	Tue Mar 18 10:42:08 1997 +0100
+++ b/src/ZF/mono.ML	Tue Mar 18 10:43:29 1997 +0100
@@ -179,12 +179,14 @@
 
 val [PQimp] = goal IFOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
-by (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by IntPr.safe_tac;
+be (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 (fast_tac (!claset addIs [PQimp RS mp]) 1);
+by IntPr.safe_tac;
+be (spec RS (PQimp RS mp)) 1;
 qed "all_mono";
 
 (*Used in intr_elim.ML and in individual datatype definitions*)