Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
changeset 58732 854eed6e5aed
parent 58676 cdf84b6e1297
child 58734 20235f0512e2 
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 21 17:23:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 21 17:23:11 2014 +0200
@@ -109,6 +109,7 @@
         co_rec_selss = [],
         co_rec_codes = [],
         co_rec_transfers = [],
+        rec_o_maps = @{thms case_sum_o_map_sum},
         common_rel_co_inducts = [],
         rel_co_inducts = [],
         common_set_inducts = [],
@@ -174,6 +175,7 @@
         co_rec_selss = [],
         co_rec_codes = [],
         co_rec_transfers = [],
+        rec_o_maps = @{thms case_prod_o_map_prod},
         common_rel_co_inducts = [],
         rel_co_inducts = [],
         common_set_inducts = [],
isabelle