equal
deleted
inserted
replaced
53 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))" |
53 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))" |
54 unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) |
54 unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) |
55 |
55 |
56 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" |
56 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" |
57 |
57 |
58 thm sum.rec_o_map |
58 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" |
59 thm sum.size_o_map |
|
60 |
|
61 thm prod.rec_o_map |
|
62 thm prod.size_o_map |
|
63 |
59 |
64 hide_const (open) xtor ctor_rec |
60 hide_const (open) xtor ctor_rec |
65 |
61 |
66 hide_fact (open) |
62 hide_fact (open) |
67 xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec |
63 xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec |