src/HOL/Relation.ML

--- a/src/HOL/Relation.ML	Mon Mar 25 08:46:02 1996 +0100
+++ b/src/HOL/Relation.ML	Mon Mar 25 11:13:59 1996 +0100
@@ -102,6 +102,10 @@
 val converse_cs = comp_cs addSIs [converseI] 
                           addSEs [converseD,converseE];
 
+goalw Relation.thy [converse_def] "converse(converse R) = R";
+by(fast_tac (prod_cs addSIs [equalityI]) 1);
+qed "converse_converse";
+
 (** Domain **)
 
 qed_goalw "Domain_iff" Relation.thy [Domain_def]