equal
deleted
inserted
replaced
585 rtac adm_subst 1 THEN |
585 rtac adm_subst 1 THEN |
586 cont_tacR 1 THEN resolve_tac prems 1), |
586 cont_tacR 1 THEN resolve_tac prems 1), |
587 strip_tac 1, |
587 strip_tac 1, |
588 rtac (rewrite_rule axs_take_def finite_ind) 1, |
588 rtac (rewrite_rule axs_take_def finite_ind) 1, |
589 ind_prems_tac prems]) |
589 ind_prems_tac prems]) |
590 handle ERROR => (warning "Cannot prove infinite induction rule"; refl)) |
590 handle ERROR _ => (warning "Cannot prove infinite induction rule"; refl)) |
591 end; (* local *) |
591 end; (* local *) |
592 |
592 |
593 (* ----- theorem concerning coinduction ------------------------------------- *) |
593 (* ----- theorem concerning coinduction ------------------------------------- *) |
594 |
594 |
595 local |
595 local |