--- 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]