# HG changeset patch
# User traytel
# Date 1347718193 -7200
# Node ID ac2e29fc57a5605081abc2776d8b7ab049aa31f7
# Parent  83b867707af2b135b1e66f54a956d76cd56d0494
export rel_mono theorem

diff -r 83b867707af2 -r ac2e29fc57a5 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 14 22:23:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Sat Sep 15 16:09:53 2012 +0200
@@ -493,6 +493,7 @@
 val rel_IdN = "rel_Id";
 val rel_GrN = "rel_Gr";
 val rel_converseN = "rel_converse";
+val rel_monoN = "rel_mono"
 val rel_ON = "rel_comp";
 val set_naturalN = "set_natural";
 val set_natural'N = "set_natural'";
@@ -1145,6 +1146,7 @@
                     (rel_IdN, [Lazy.force (#rel_Id facts)]),
                     (rel_GrN, [Lazy.force (#rel_Gr facts)]),
                     (rel_converseN, [Lazy.force (#rel_converse facts)]),
+                    (rel_monoN, [Lazy.force (#rel_mono facts)]),
                     (rel_ON, [Lazy.force (#rel_O facts)]),
                     (map_id'N, [Lazy.force (#map_id' facts)]),
                     (map_comp'N, [Lazy.force (#map_comp' facts)]),