451 (** theory setup **) |
451 (** theory setup **) |
452 |
452 |
453 val setup = |
453 val setup = |
454 [GlobalInduct.init, LocalInduct.init, |
454 [GlobalInduct.init, LocalInduct.init, |
455 Attrib.add_attributes |
455 Attrib.add_attributes |
456 [(casesN, cases_attr, "cases rule for type or set"), |
456 [(casesN, cases_attr, "declaration of cases rule for type or set"), |
457 (inductN, induct_attr, "induction rule for type or set")], |
457 (inductN, induct_attr, "declaration of induction rule for type or set")], |
458 Method.add_methods |
458 Method.add_methods |
459 [("cases", cases_meth oo cases_args, "case analysis on types or sets"), |
459 [("cases", cases_meth oo cases_args, "case analysis on types or sets"), |
460 ("induct", induct_meth oo induct_args, "induction on types or sets")], |
460 ("induct", induct_meth oo induct_args, "induction on types or sets")], |
461 (#1 o PureThy.add_thms [(("case_split", case_split), [])])]; |
461 (#1 o PureThy.add_thms [(("case_split", case_split), [])])]; |
462 |
462 |