# HG changeset patch # User blanchet # Date 1410790454 -7200 # Node ID ea3d989219b4e68554d55001c423398d1ee60e33 # Parent 1defb39ab329be42af7f413b28bcd5c1f2a5dd9f set 'mono' attribute on 'rel_mono' diff -r 1defb39ab329 -r ea3d989219b4 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 15 16:11:01 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 15 16:14:14 2014 +0200 @@ -973,9 +973,9 @@ @{thm list.rel_map(1)[no_vars]} \\ @{thm list.rel_map(2)[no_vars]} -\item[@{text "t."}\hthm{rel_mono} @{text "[relator_mono]"}\rm:] ~ \\ +\item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\ @{thm list.rel_mono[no_vars]} \\ -(The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin, +(The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin, Section~\ref{ssec:lifting}.) \item[@{text "t."}\hthm{rel_transfer}\rm:] ~ \\ diff -r 1defb39ab329 -r ea3d989219b4 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 15 16:11:01 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 15 16:14:14 2014 +0200 @@ -152,6 +152,7 @@ open BNF_Def_Tactics val fundefcong_attrs = @{attributes [fundef_cong]}; +val mono_attrs = @{attributes [mono]}; type axioms = { map_id0: thm, @@ -730,7 +731,7 @@ (rel_flipN, [Lazy.force (#rel_flip facts)], []), (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), (rel_mapN, Lazy.force (#rel_map facts), []), - (rel_monoN, [Lazy.force (#rel_mono facts)], []), + (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs), (rel_transferN, [Lazy.force (#rel_transfer facts)], []), (set_mapN, map Lazy.force (#set_map facts), []), (set_transferN, Lazy.force (#set_transfer facts), [])]