# HG changeset patch
# User desharna
# Date 1635857489 -3600
# Node ID d4ef127b74df85dc9f7cd39763c564670b518bb9
# Parent  b74dfca75e84065d24f111bd73f31925fe661c57
added "mono" attribute to BNF generated pred_mono theorems

diff -r b74dfca75e84 -r d4ef127b74df src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Nov 02 08:30:08 2021 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Nov 02 13:51:29 2021 +0100
@@ -940,8 +940,8 @@
            (map_id0N, [#map_id0 axioms], []),
            (map_transferN, [Lazy.force (#map_transfer facts)], []),
            (map_identN, [Lazy.force (#map_ident facts)], []),
+           (pred_monoN, [Lazy.force (#pred_mono facts)], mono_attrs),
            (pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []),
-           (pred_monoN, [Lazy.force (#pred_mono facts)], []),
            (pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs),
            (pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []),
            (pred_mapN, [Lazy.force (#pred_map facts)], []),