# HG changeset patch
# User nipkow
# Date 827748839 -3600
# Node ID 248e1e125ca062ebf47c872ea1dd2e04649be162
# Parent  cff41d1094adebab41f6b816176b20458879acb5
added converse_converse

diff -r cff41d1094ad -r 248e1e125ca0 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]