export rel_mono theorem
authortraytel
Sat Sep 15 16:09:53 2012 +0200 (2012-09-15)
changeset 49386ac2e29fc57a5
parent 49385 83b867707af2
child 49387 167708456269
export rel_mono theorem
src/HOL/Codatatype/Tools/bnf_def.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 14 22:23:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Sat Sep 15 16:09:53 2012 +0200
     1.3 @@ -493,6 +493,7 @@
     1.4  val rel_IdN = "rel_Id";
     1.5  val rel_GrN = "rel_Gr";
     1.6  val rel_converseN = "rel_converse";
     1.7 +val rel_monoN = "rel_mono"
     1.8  val rel_ON = "rel_comp";
     1.9  val set_naturalN = "set_natural";
    1.10  val set_natural'N = "set_natural'";
    1.11 @@ -1145,6 +1146,7 @@
    1.12                      (rel_IdN, [Lazy.force (#rel_Id facts)]),
    1.13                      (rel_GrN, [Lazy.force (#rel_Gr facts)]),
    1.14                      (rel_converseN, [Lazy.force (#rel_converse facts)]),
    1.15 +                    (rel_monoN, [Lazy.force (#rel_mono facts)]),
    1.16                      (rel_ON, [Lazy.force (#rel_O facts)]),
    1.17                      (map_id'N, [Lazy.force (#map_id' facts)]),
    1.18                      (map_comp'N, [Lazy.force (#map_comp' facts)]),