380 fun add_cases_induct no_elim no_ind names elims induct induct_cases = |
380 fun add_cases_induct no_elim no_ind names elims induct induct_cases = |
381 let |
381 let |
382 fun cases_spec (name, elim) thy = |
382 fun cases_spec (name, elim) thy = |
383 thy |
383 thy |
384 |> Theory.add_path (Sign.base_name name) |
384 |> Theory.add_path (Sign.base_name name) |
385 |> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])]) |
385 |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])]) |
386 |> Theory.parent_path; |
386 |> Theory.parent_path; |
387 val cases_specs = if no_elim then [] else map2 cases_spec (names, elims); |
387 val cases_specs = if no_elim then [] else map2 cases_spec (names, elims); |
388 |
388 |
389 fun induct_spec (name, th) = (#1 o PureThy.add_thms |
389 fun induct_spec (name, th) = (#1 o PureThy.add_thms |
390 [(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]); |
390 [(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]); |
391 val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); |
391 val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); |
392 in Library.apply (cases_specs @ induct_specs) end; |
392 in Library.apply (cases_specs @ induct_specs) end; |
393 |
393 |
394 |
394 |
395 |
395 |