src/HOL/Relation.ML
changeset 1605 248e1e125ca0
parent 1552 6f71b5d46700
child 1642 21db0cf9a1a4
     1.1 --- a/src/HOL/Relation.ML	Mon Mar 25 08:46:02 1996 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Mar 25 11:13:59 1996 +0100
     1.3 @@ -102,6 +102,10 @@
     1.4  val converse_cs = comp_cs addSIs [converseI] 
     1.5                            addSEs [converseD,converseE];
     1.6  
     1.7 +goalw Relation.thy [converse_def] "converse(converse R) = R";
     1.8 +by(fast_tac (prod_cs addSIs [equalityI]) 1);
     1.9 +qed "converse_converse";
    1.10 +
    1.11  (** Domain **)
    1.12  
    1.13  qed_goalw "Domain_iff" Relation.thy [Domain_def]