--- 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:] ~ \\
--- 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), [])]