Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export rel_mono theorem
authortraytel
Sat, 15 Sep 2012 16:09:53 +0200
changeset 49386 ac2e29fc57a5
parent 49385 83b867707af2
child 49387 167708456269
export rel_mono theorem
src/HOL/Codatatype/Tools/bnf_def.ML file | annotate | diff | comparison | revisions 
--- 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)]),
isabelle