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.
note map_id0 more often
authordesharna
Thu, 08 May 2014 12:54:02 +0200
changeset 56954 4ce75d6a8935
parent 56953 e503d80f7f35
child 56955 ddcfa5d19c1a
note map_id0 more often
src/HOL/Tools/BNF/bnf_def.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed May 14 11:33:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu May 08 12:54:02 2014 +0200
@@ -640,7 +640,6 @@
             (in_relN, [Lazy.force (#in_rel facts)]),
             (inj_mapN, [Lazy.force (#inj_map facts)]),
             (map_comp0N, [#map_comp0 axioms]),
-            (map_id0N, [#map_id0 axioms]),
             (map_transferN, [Lazy.force (#map_transfer facts)]),
             (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
             (set_map0N, #set_map0 axioms),
@@ -661,6 +660,7 @@
             (map_cong0N, [#map_cong0 axioms], []),
             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
             (map_idN, [Lazy.force (#map_id facts)], []),
+            (map_id0N, [#map_id0 axioms], []),
             (map_identN, [Lazy.force (#map_ident facts)], []),
             (rel_comppN, [Lazy.force (#rel_OO facts)], []),
             (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
isabelle