equal
deleted
inserted
replaced
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.$$$ "add" -- Args.colon >> K (I, split_add_local), |
421 Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)]; |
421 Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)]; |
422 |
422 |
423 val split_meth = Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o split_tac); |
423 val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms); |
|
424 |
|
425 fun split_meth (asm, ths) = |
|
426 Method.SIMPLE_METHOD' HEADGOAL (if asm then split_asm_tac ths else split_tac ths); |
424 |
427 |
425 |
428 |
426 |
429 |
427 (** theory setup **) |
430 (** theory setup **) |
428 |
431 |
429 val setup = |
432 val setup = |
430 [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")], |
433 [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")], |
431 Method.add_methods [(splitN, split_meth, "apply splitter rule")]]; |
434 Method.add_methods [(splitN, split_meth oo split_args, "apply splitter rule")]]; |
432 |
435 |
433 end; |
436 end; |