equal
deleted
inserted
replaced
415 |
415 |
416 (* methods *) |
416 (* methods *) |
417 |
417 |
418 val split_modifiers = |
418 val split_modifiers = |
419 [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier), |
419 [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier), |
420 Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local), |
420 Args.$$$ splitN -- Args.$$$ Args.addN -- Args.colon >> K (I, split_add_local), |
421 Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)]; |
421 Args.$$$ splitN -- Args.$$$ Args.delN -- Args.colon >> K (I, split_del_local)]; |
422 |
422 |
423 val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms); |
423 val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms); |
424 |
424 |
425 fun split_meth (asm, ths) = |
425 fun split_meth (asm, ths) = |
426 Method.SIMPLE_METHOD' HEADGOAL (if asm then split_asm_tac ths else split_tac ths); |
426 Method.SIMPLE_METHOD' HEADGOAL (if asm then split_asm_tac ths else split_tac ths); |