equal
deleted
inserted
replaced
475 Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), |
475 Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), |
476 Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; |
476 Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; |
477 |
477 |
478 fun split_meth src = |
478 fun split_meth src = |
479 Method.syntax Attrib.thms src |
479 Method.syntax Attrib.thms src |
480 #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths)); |
480 #> (fn (_, ths) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)); |
481 |
481 |
482 |
482 |
483 (* theory setup *) |
483 (* theory setup *) |
484 |
484 |
485 val setup = |
485 val setup = |