# HG changeset patch
# User paulson
# Date 855574494 -3600
# Node ID 5ac837d98a8512ebd68d32a4cd6d92053cae8b68
# Parent  b301958c465d6e10aac34753d0206dc987e21c67
Renamed structure Int (intuitionistic prover) to IntPr

diff -r b301958c465d -r 5ac837d98a85 src/ZF/mono.ML
--- a/src/ZF/mono.ML	Mon Feb 10 12:31:54 1997 +0100
+++ b/src/ZF/mono.ML	Mon Feb 10 12:34:54 1997 +0100
@@ -161,15 +161,15 @@
 qed "in_mono";
 
 goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
-by (Int.fast_tac 1);
+by (IntPr.fast_tac 1);
 qed "conj_mono";
 
 goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
-by (Int.fast_tac 1);
+by (IntPr.fast_tac 1);
 qed "disj_mono";
 
 goal IFOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
-by (Int.fast_tac 1);
+by (IntPr.fast_tac 1);
 qed "imp_mono";
 
 goal IFOL.thy "P-->P";