equal
deleted
inserted
replaced
139 let val r = length kks in |
139 let val r = length kks in |
140 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt, |
140 EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac ctxt, |
141 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
141 REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN |
142 EVERY [REPEAT_DETERM_N r |
142 EVERY [REPEAT_DETERM_N r |
143 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
143 (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2), |
144 if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1, |
144 if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, atac 1, |
145 mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs] |
145 mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs] |
146 end; |
146 end; |
147 |
147 |
148 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss = |
148 fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss = |
149 let val n = Integer.sum ns in |
149 let val n = Integer.sum ns in |