# HG changeset patch
# User wenzelm
# Date 877002149 -7200
# Node ID 2a2a86b57fed6d13d4207a00884f89b178df401c
# Parent  59bab7a52b4c1d2252b2ebbd37d40a59fde83e86
sevaral goals restated in mono.thy;

diff -r 59bab7a52b4c -r 2a2a86b57fed src/ZF/mono.ML
--- a/src/ZF/mono.ML	Thu Oct 16 13:39:20 1997 +0200
+++ b/src/ZF/mono.ML	Thu Oct 16 13:42:29 1997 +0200
@@ -78,25 +78,25 @@
 
 (** Quine-inspired ordered pairs, products, injections and sums **)
 
-goalw QPair.thy [QPair_def] "!!a b c d. [| a<=c;  b<=d |] ==> <a;b> <= <c;d>";
+goalw thy [QPair_def] "!!a b c d. [| a<=c;  b<=d |] ==> <a;b> <= <c;d>";
 by (REPEAT (ares_tac [sum_mono] 1));
 qed "QPair_mono";
 
-goal QPair.thy "!!A B C D. [| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
+goal thy "!!A B C D. [| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
 \                          QSigma(A,B) <= QSigma(C,D)";
 by (Blast_tac 1);
 qed "QSigma_mono_lemma";
 val QSigma_mono = ballI RSN (2,QSigma_mono_lemma);
 
-goalw QPair.thy [QInl_def] "!!a b. a<=b ==> QInl(a) <= QInl(b)";
+goalw thy [QInl_def] "!!a b. a<=b ==> QInl(a) <= QInl(b)";
 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
 qed "QInl_mono";
 
-goalw QPair.thy [QInr_def] "!!a b. a<=b ==> QInr(a) <= QInr(b)";
+goalw thy [QInr_def] "!!a b. a<=b ==> QInr(a) <= QInr(b)";
 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
 qed "QInr_mono";
 
-goal QPair.thy "!!A B C D. [| A<=C;  B<=D |] ==> A <+> B <= C <+> D";
+goal thy "!!A B C D. [| A<=C;  B<=D |] ==> A <+> B <= C <+> D";
 by (Blast_tac 1);
 qed "qsum_mono";