# HG changeset patch
# User paulson
# Date 905441802 -7200
# Node ID 2ea5d254e44e2a268256690bc5abf854fb5b52a2
# Parent  cc95f12ab64fe8d73de6d6d3c2dffe4976cd2893
eliminated equals0E

diff -r cc95f12ab64f -r 2ea5d254e44e src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Thu Sep 10 17:34:43 1998 +0200
+++ b/src/ZF/Perm.ML	Thu Sep 10 17:36:42 1998 +0200
@@ -462,14 +462,14 @@
 (** Unions of functions -- cf similar theorems on func.ML **)
 
 (*Theorem by KG, proof by LCP*)
-Goal "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] ==> \
-\           (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
+Goal "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] \
+\     ==> (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
 by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
         lam_injective 1);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] 
                          setloop (split_tac [split_if] ORELSE' etac UnE))));
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type] addDs [equals0E]) 1);
+by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
 qed "inj_disjoint_Un";
 
 Goalw [surj_def]