equal
deleted
inserted
replaced
565 val ks = 1 upto n; |
565 val ks = 1 upto n; |
566 fun mk_inner_induct_tac induct i = |
566 fun mk_inner_induct_tac induct i = |
567 EVERY' [rtac allI, fo_rtac induct ctxt, |
567 EVERY' [rtac allI, fo_rtac induct ctxt, |
568 select_prem_tac n (dtac @{thm meta_spec2}) i, |
568 select_prem_tac n (dtac @{thm meta_spec2}) i, |
569 REPEAT_DETERM_N n o |
569 REPEAT_DETERM_N n o |
570 EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac, |
570 EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt, |
571 REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac], |
571 REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac], |
572 atac]; |
572 atac]; |
573 in |
573 in |
574 EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts ctor_induct), |
574 EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts ctor_induct), |
575 EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac impI, |
575 EVERY' (map2 mk_inner_induct_tac weak_ctor_inducts ks), rtac impI, |