src/HOL/Relation.ML
changeset 1761 29e08d527ba1
parent 1754 852093aeb0ab
child 1786 8a31d85d27b8
     1.1 --- a/src/HOL/Relation.ML	Thu May 23 14:37:06 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu May 23 15:15:20 1996 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4                            addSEs [converseD,converseE];
     1.5  
     1.6  goalw Relation.thy [converse_def] "converse(converse R) = R";
     1.7 -by(fast_tac (!claset addSIs [equalityI]) 1);
     1.8 +by(Fast_tac 1);
     1.9  qed "converse_converse";
    1.10  
    1.11  (** Domain **)