Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Relation.ML
changeset 1761 29e08d527ba1
parent 1754 852093aeb0ab
child 1786 8a31d85d27b8 
--- a/src/HOL/Relation.ML	Thu May 23 14:37:06 1996 +0200
+++ b/src/HOL/Relation.ML	Thu May 23 15:15:20 1996 +0200
@@ -110,7 +110,7 @@
                           addSEs [converseD,converseE];
 
 goalw Relation.thy [converse_def] "converse(converse R) = R";
-by(fast_tac (!claset addSIs [equalityI]) 1);
+by(Fast_tac 1);
 qed "converse_converse";
 
 (** Domain **)
isabelle