# HG changeset patch
# User paulson
# Date 858678209 -3600
# Node ID 734fc343ec2a6f3790ff484b112f12e90bc26117
# Parent  f119c3686782cfe54f4a448f69013fb78ad6b91f
Conducted the IFOL proofs using intuitionistic tools

diff -r f119c3686782 -r 734fc343ec2a src/ZF/mono.ML
--- 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*)