note 'inj_map' more often
authordesharna
Mon Aug 18 13:49:47 2014 +0200 (2014-08-18)
changeset 579691e7b9579b14f
parent 57968 00e9c6d367e7
child 57970 eaa986cd285a
note 'inj_map' more often
src/Doc/Datatypes/Datatypes.thy
src/HOL/Tools/BNF/bnf_def.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 13:46:26 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 18 13:49:47 2014 +0200
     1.3 @@ -913,6 +913,9 @@
     1.4  \begin{indentblock}
     1.5  \begin{description}
     1.6  
     1.7 +\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
     1.8 +@{thm list.inj_map[no_vars]}
     1.9 +
    1.10  \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
    1.11  @{thm list.set_map[no_vars]}
    1.12  
     2.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:26 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:49:47 2014 +0200
     2.3 @@ -659,7 +659,6 @@
     2.4             (in_bdN, [Lazy.force (#in_bd facts)]),
     2.5             (in_monoN, [Lazy.force (#in_mono facts)]),
     2.6             (in_relN, [Lazy.force (#in_rel facts)]),
     2.7 -           (inj_mapN, [Lazy.force (#inj_map facts)]),
     2.8             (map_comp0N, [#map_comp0 axioms]),
     2.9             (map_transferN, [Lazy.force (#map_transfer facts)]),
    2.10             (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
    2.11 @@ -677,7 +676,8 @@
    2.12      fun note_unless_dont_note (noted0, lthy0) =
    2.13        let
    2.14          val notes =
    2.15 -          [(map_compN, [Lazy.force (#map_comp facts)], []),
    2.16 +          [(inj_mapN, [Lazy.force (#inj_map facts)], []),
    2.17 +           (map_compN, [Lazy.force (#map_comp facts)], []),
    2.18             (map_cong0N, [#map_cong0 axioms], []),
    2.19             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
    2.20             (map_idN, [Lazy.force (#map_id facts)], []),