--- a/src/ZF/Perm.ML Wed Jan 05 19:47:14 1994 +0100
+++ b/src/ZF/Perm.ML Fri Jan 07 10:59:51 1994 +0100
@@ -194,6 +194,11 @@
by (fast_tac comp_cs 1);
val domain_comp_eq = result();
+goal Perm.thy "(r O s)``A = r``(s``A)";
+by (fast_tac (comp_cs addIs [equalityI]) 1);
+val image_comp = result();
+
+
(** Other results **)
goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
--- a/src/ZF/perm.ML Wed Jan 05 19:47:14 1994 +0100
+++ b/src/ZF/perm.ML Fri Jan 07 10:59:51 1994 +0100
@@ -194,6 +194,11 @@
by (fast_tac comp_cs 1);
val domain_comp_eq = result();
+goal Perm.thy "(r O s)``A = r``(s``A)";
+by (fast_tac (comp_cs addIs [equalityI]) 1);
+val image_comp = result();
+
+
(** Other results **)
goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";