equal
deleted
inserted
replaced
396 |
396 |
397 |
397 |
398 fun induct_scheme_tac ctxt = |
398 fun induct_scheme_tac ctxt = |
399 mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; |
399 mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; |
400 |
400 |
401 val setup = Method.add_methods |
401 val setup = |
402 [("induct_scheme", Method.ctxt_args (RAW_METHOD o induct_scheme_tac), |
402 Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac)) |
403 "proves an induction principle")] |
403 "proves an induction principle" |
404 |
404 |
405 end |
405 end |