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.
merged
authortraytel
Tue, 21 Jan 2014 13:27:50 +0100
changeset 55097 81dac5c1a5bb
parent 55096 916b2ac758f4 (current diff)
parent 55095 7883bd17362f (diff)
child 55098 01869d711567
merged
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:21:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:27:50 2014 +0100
@@ -341,7 +341,8 @@
 
 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
   ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
-   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
+   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs))
+  : lfp_sugar_thms;
 
 val transfer_lfp_sugar_thms =
   morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
isabelle