equal
deleted
inserted
replaced
465 THEN' eqvt_tac ctxt (eqvt_relaxed_config addexcls const_names) |
465 THEN' eqvt_tac ctxt (eqvt_relaxed_config addexcls const_names) |
466 THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym])))) |
466 THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym])))) |
467 |
467 |
468 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
468 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
469 HEADGOAL |
469 HEADGOAL |
470 (Object_Logic.full_atomize_tac |
470 (Object_Logic.full_atomize_tac ctxt |
471 THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) |
471 THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) |
472 THEN_ALL_NEW subproof_tac const_names simps ctxt) |
472 THEN_ALL_NEW subproof_tac const_names simps ctxt) |
473 |
473 |
474 fun mk_eqvt_goal pi const arg = |
474 fun mk_eqvt_goal pi const arg = |
475 let |
475 let |