# HG changeset patch
# User lcp
# Date 787486669 -3600
# Node ID 354a56e923ffaac770f1f2f25bc4f93124f5bf29
# Parent  4c10e8532d43984f7b35d343d5e5226a06d57922
updated comment;
renamed converse_of_Un to converse_Un

diff -r 4c10e8532d43 -r 354a56e923ff src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Thu Dec 15 11:08:22 1994 +0100
+++ b/src/ZF/Perm.ML	Thu Dec 15 11:17:49 1994 +0100
@@ -223,7 +223,7 @@
 
 (** Composition of two relations **)
 
-(*The inductive definition package could derive these theorems for R o S*)
+(*The inductive definition package could derive these theorems for (r O s)*)
 
 goalw Perm.thy [comp_def] "!!r s. [| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
 by (fast_tac ZF_cs 1);
@@ -444,7 +444,7 @@
 by (DEPTH_SOLVE_1 
       (resolve_tac [Un_least,converse_mono, Un_upper1,Un_upper2] 2));
 by (fast_tac ZF_cs 1);
-qed "converse_of_Un";
+qed "converse_Un";
 
 goalw Perm.thy [surj_def]
     "!!f g. [| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
@@ -461,7 +461,7 @@
     "!!f g. [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
 \           (f Un g) : bij(A Un C, B Un D)";
 by (rtac invertible_imp_bijective 1);
-by (rtac (converse_of_Un RS ssubst) 1);
+by (rtac (converse_Un RS ssubst) 1);
 by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
 qed "bij_disjoint_Un";