Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Renamed structure Int (intuitionistic prover) to IntPr
authorpaulson
Mon, 10 Feb 1997 12:34:54 +0100
changeset 2602 5ac837d98a85
parent 2601 b301958c465d
child 2603 4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr
src/ZF/mono.ML file | annotate | diff | comparison | revisions 
--- 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";
isabelle