equal
deleted
inserted
replaced
465 val split_modifiers = |
465 val split_modifiers = |
466 [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier), |
466 [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier), |
467 Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), |
467 Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), |
468 Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; |
468 Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; |
469 |
469 |
470 fun split_meth parser = (Attrib.thms >> |
|
471 (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser; |
|
472 |
|
473 |
470 |
474 (* theory setup *) |
471 (* theory setup *) |
475 |
472 |
476 val setup = |
473 val setup = |
477 Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #> |
474 Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #> |
478 Method.setup @{binding split} split_meth "apply case split rule"; |
475 Method.setup @{binding split} |
|
476 (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) |
|
477 "apply case split rule"; |
479 |
478 |
480 end; |
479 end; |