equal
deleted
inserted
replaced
446 [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier), |
446 [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier), |
447 Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), |
447 Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add), |
448 Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; |
448 Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; |
449 |
449 |
450 fun split_meth src = |
450 fun split_meth src = |
451 Method.syntax Attrib.local_thms src |
451 Method.syntax Attrib.thms src |
452 #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths)); |
452 #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths)); |
453 |
453 |
454 |
454 |
455 (* theory setup *) |
455 (* theory setup *) |
456 |
456 |