Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Deleted call to flexflex_tac
authorlcp
Thu, 06 Apr 1995 12:06:09 +0200
changeset 1013 be30ddf0c9b4
parent 1012 db0563a1644a
child 1014 8bec0698d58c
Deleted call to flexflex_tac
src/ZF/EquivClass.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/EquivClass.ML	Thu Apr 06 12:03:01 1995 +0200
+++ b/src/ZF/EquivClass.ML	Thu Apr 06 12:06:09 1995 +0200
@@ -39,7 +39,6 @@
 by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 3);
 by (ALLGOALS (fast_tac 
 	      (ZF_cs addSIs [converseI] addIs [compI] addSEs [compE])));
-by flexflex_tac;
 qed "comp_equivI";
 
 (** Equivalence classes **)
isabelle