author lcp Thu, 15 Dec 1994 11:17:49 +0100 changeset 791 354a56e923ff parent 790 4c10e8532d43 child 792 5d2a7634da46
updated comment; renamed converse_of_Un to converse_Un
 src/ZF/Perm.ML file | annotate | diff | comparison | revisions
--- 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";