equal
deleted
inserted
replaced
104 end; |
104 end; |
105 |
105 |
106 val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs; |
106 val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs; |
107 |
107 |
108 fun mk_case_transfer_tac ctxt rel_cases cases = |
108 fun mk_case_transfer_tac ctxt rel_cases cases = |
109 let |
109 let val n = length (tl (Thm.prems_of rel_cases)) in |
110 val n = length (tl (Thm.prems_of rel_cases)); |
|
111 in |
|
112 REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN |
110 REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN |
113 HEADGOAL (etac rel_cases) THEN |
111 HEADGOAL (etac rel_cases) THEN |
114 ALLGOALS (hyp_subst_tac ctxt) THEN |
112 ALLGOALS (hyp_subst_tac ctxt) THEN |
115 unfold_thms_tac ctxt cases THEN |
113 unfold_thms_tac ctxt cases THEN |
116 ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k) k) THEN |
114 ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k) k) THEN |