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.
Quot/QuotList.thy
changeset 768 e9e205b904e2
parent 668 ef5b941f00e2
child 796 64f9c76f70c7 
--- a/Quot/QuotList.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/QuotList.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -59,7 +59,7 @@
   apply(rule list_rel_rel[OF q])
   done
 
-lemma map_id: "map id \<equiv> id"
+lemma map_id[id_simps]: "map id \<equiv> id"
   apply (rule eq_reflection)
   apply (rule ext)
   apply (rule_tac list="x" in list.induct)
nominal2