Mercurial Mercurial > hg > nominal2 / 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.
QuotMain.thy
changeset 539 8287fb5b8d7a
parent 537 57073b0b8fac
child 540 c0b13fb70d6d 
--- a/QuotMain.thy	Fri Dec 04 16:01:23 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:12:40 2009 +0100
@@ -461,7 +461,7 @@
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
      rtac @{thm IDENTITY_equivp},
-     rtac @{thm LIST_equivp}])
+     rtac @{thm list_equivp}])
 *}
 
 ML {*
nominal2