equal
deleted
inserted
replaced
63 fun mk_unabs_def_unused_0 n = |
63 fun mk_unabs_def_unused_0 n = |
64 funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); |
64 funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); |
65 |
65 |
66 val rec_o_map_simp_thms = |
66 val rec_o_map_simp_thms = |
67 @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod |
67 @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod |
68 BNF_Comp.id_bnf_comp_def}; |
68 BNF_Composition.id_bnf_comp_def}; |
69 |
69 |
70 fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses |
70 fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses |
71 ctor_rec_o_map = |
71 ctor_rec_o_map = |
72 unfold_thms_tac ctxt [rec_def] THEN |
72 unfold_thms_tac ctxt [rec_def] THEN |
73 HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN' |
73 HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN' |