# 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), [])]