# HG changeset patch
# User paulson
# Date 810319962 -7200
# Node ID 79692e8ce183b086d7a3f3731f3445108cfa43dd
# Parent  18b1441fb603855660e33fb00b44033cfc8b6860
Removed duplicate copy of converse_Un

diff -r 18b1441fb603 -r 79692e8ce183 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Sep 01 14:27:36 1995 +0200
+++ b/src/ZF/Perm.ML	Tue Sep 05 18:52:42 1995 +0200
@@ -459,13 +459,6 @@
 
 (** Unions of functions -- cf similar theorems on func.ML **)
 
-goal Perm.thy "converse(r Un s) = converse(r) Un converse(s)";
-by (rtac equalityI 1);
-by (DEPTH_SOLVE_1 
-      (resolve_tac [Un_least,converse_mono, Un_upper1,Un_upper2] 2));
-by (fast_tac ZF_cs 1);
-qed "converse_Un";
-
 goalw Perm.thy [surj_def]
     "!!f g. [| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
 \           (f Un g) : surj(A Un C, B Un D)";