added converse_converse
authornipkow
Mon Mar 25 11:13:59 1996 +0100 (1996-03-25)
changeset 1605248e1e125ca0
parent 1604 cff41d1094ad
child 1606 dd66bed09592
added converse_converse
src/HOL/Relation.ML
     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]