Converted back from upair.thy to ZF.thy

--- a/src/ZF/AC/AC7_AC9.ML	Wed Apr 02 15:28:42 1997 +0200
+++ b/src/ZF/AC/AC7_AC9.ML	Wed Apr 02 15:29:48 1997 +0200
@@ -13,7 +13,7 @@
 (*  - Sigma_fun_space_eqpoll                                              *)
 (* ********************************************************************** *)
 
-goal upair.thy "!!A. [| C~:A; B:A |] ==> B~=C";
+goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
 by (Fast_tac 1);
 val mem_not_eq_not_mem = result();
 

--- a/src/ZF/AC/AC_Equiv.ML	Wed Apr 02 15:28:42 1997 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Wed Apr 02 15:29:48 1997 +0200
@@ -44,7 +44,7 @@
 
 (* used only in WO1_DC.ML *)
 (*Note simpler proof*)
-goal upair.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
+goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg;  \
 \         A<=Df; A<=Dg |] ==> f``A=g``A";
 by (asm_simp_tac (!simpset addsimps [image_fun]) 1);
 val images_eq = result();

--- a/src/ZF/AC/Cardinal_aux.ML	Wed Apr 02 15:28:42 1997 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML	Wed Apr 02 15:29:48 1997 +0200
@@ -68,11 +68,11 @@
 val ss = (!simpset) addsimps [inj_is_fun RS apply_type, left_inverse] 
                setloop (split_tac [expand_if] ORELSE' etac UnE);
 
-goal upair.thy "{x, y} - {y} = {x} - {y}";
+goal ZF.thy "{x, y} - {y} = {x} - {y}";
 by (Fast_tac 1);
 val double_Diff_sing = result();
 
-goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
+goal ZF.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
 by (split_tac [expand_if] 1);
 by (asm_full_simp_tac (!simpset addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
 by (fast_tac (!claset addSIs [the_equality] addEs [equalityE]) 1);

--- 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();
 

--- a/src/ZF/ex/PropLog.ML	Wed Apr 02 15:28:42 1997 +0200
+++ b/src/ZF/ex/PropLog.ML	Wed Apr 02 15:29:48 1997 +0200
@@ -236,11 +236,11 @@
 
 (** Two lemmas for use with weaken_left **)
 
-goal upair.thy "B-C <= cons(a, B-cons(a,C))";
+goal ZF.thy "B-C <= cons(a, B-cons(a,C))";
 by (Fast_tac 1);
 qed "cons_Diff_same";
 
-goal upair.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
+goal ZF.thy "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
 by (Fast_tac 1);
 qed "cons_Diff_subset2";