src/ZF/equalities.ML
 changeset 1056 097b3255bf3a parent 1035 279a4fd3c5ce child 1461 6bcb44e4d6e5
--- a/src/ZF/equalities.ML	Fri Apr 14 11:24:10 1995 +0200
+++ b/src/ZF/equalities.ML	Fri Apr 14 11:24:51 1995 +0200
@@ -336,7 +336,7 @@

goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
by (fast_tac eq_cs 1);
-qed "domain_diff_subset";
+qed "domain_Diff_subset";

goal ZF.thy "domain(converse(r)) = range(r)";
by (fast_tac eq_cs 1);
@@ -367,7 +367,7 @@

goal ZF.thy "range(A) - range(B) <= range(A - B)";
by (fast_tac eq_cs 1);
-qed "range_diff_subset";
+qed "range_Diff_subset";

goal ZF.thy "range(converse(r)) = domain(r)";
by (fast_tac eq_cs 1);
@@ -395,7 +395,7 @@

goal ZF.thy "field(A) - field(B) <= field(A - B)";
by (fast_tac eq_cs 1);
-qed "field_diff_subset";
+qed "field_Diff_subset";

(** Image **)
@@ -456,7 +456,7 @@

goal ZF.thy "converse(A) - converse(B) = converse(A - B)";
by (fast_tac eq_cs 1);
-qed "converse_diff";
+qed "converse_Diff";

(*Does the analogue hold for INT?*)
goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";