src/ZF/AC/WO6_WO1.ML
changeset 2873 5f0599e15448
parent 2493 bdeb5024353a
child 3731 71366483323b
--- a/src/ZF/AC/WO6_WO1.ML	Wed Apr 02 15:28:42 1997 +0200
+++ b/src/ZF/AC/WO6_WO1.ML	Wed Apr 02 15:29:48 1997 +0200
@@ -174,7 +174,7 @@
 by (fast_tac (!claset addSEs [LeastI, lt_Ord]) 1);
 val uu_not_empty = result();
 
-goal upair.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
+goal ZF.thy "!!r. [| r<=A*B; r~=0 |] ==> domain(r)~=0";
 by (REPEAT (eresolve_tac [asm_rl, not_emptyE, subsetD RS SigmaE, 
                 sym RSN (2, subst_elem) RS domainI RS not_emptyI] 1));
 val not_empty_rel_imp_domain = result();
@@ -188,7 +188,7 @@
         THEN (REPEAT (ares_tac [lt_Ord] 1)));
 val Least_uu_not_empty_lt_a = result();
 
-goal upair.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
+goal ZF.thy "!!B. [| B<=A; a~:B |] ==> B <= A-{a}";
 by (Fast_tac 1);
 val subset_Diff_sing = result();