# HG changeset patch
# User lcp
# Date 787581888 -3600
# Node ID d689e796d1863328c424b110f82164c30365d0ec
# Parent  349d41ffa378411828d07fe0028f3cfbc3ba0fd6
converse_converse, converse_prod: renamed from
converse_of_converse, converse_of_prod

diff -r 349d41ffa378 -r d689e796d186 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Fri Dec 16 13:43:01 1994 +0100
+++ b/src/ZF/domrange.ML	Fri Dec 16 13:44:48 1994 +0100
@@ -33,14 +33,14 @@
 val converse_cs = pair_cs addSIs [converseI] 
 			  addSEs [converseD,converseE];
 
-qed_goal "converse_of_converse" ZF.thy
+qed_goal "converse_converse" ZF.thy
     "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
  (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
 
 qed_goal "converse_type" ZF.thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
  (fn _ => [ (fast_tac converse_cs 1) ]);
 
-qed_goal "converse_of_prod" ZF.thy "converse(A*B) = B*A"
+qed_goal "converse_prod" ZF.thy "converse(A*B) = B*A"
  (fn _ => [ (fast_tac (converse_cs addSIs [equalityI]) 1) ]);
 
 qed_goal "converse_empty" ZF.thy "converse(0) = 0"
@@ -79,7 +79,7 @@
 
 qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
  (fn _ =>
-  [ (rtac (converse_of_prod RS ssubst) 1),
+  [ (rtac (converse_prod RS ssubst) 1),
     (rtac domain_subset 1) ]);