# HG changeset patch
# User lcp
# Date 797851491 -7200
# Node ID 097b3255bf3a10ddeb498a13ca46fd4f1fb90b42
# Parent  67f5344605b7327a784f84b57dd9480ab25b9fcf
Renamed domain_diff_subset, range_diff_subset,
field_diff_subset, converse_diff to domain_Diff_subset, range_Diff_subset,
field_Diff_subset, converse_Diff for consistency. (Thanks to KG)

diff -r 67f5344605b7 -r 097b3255bf3a src/ZF/equalities.ML
--- 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)))";