equal
deleted
inserted
replaced
485 Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local), |
485 Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local), |
486 Args.$$$ otherN >> K (I, I)]; |
486 Args.$$$ otherN >> K (I, I)]; |
487 |
487 |
488 fun simp_method tac = |
488 fun simp_method tac = |
489 (fn prems => fn ctxt => Method.METHOD (fn facts => |
489 (fn prems => fn ctxt => Method.METHOD (fn facts => |
490 FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) |
490 HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) |
491 |> Method.bang_sectioned_args simp_modifiers'; |
491 |> Method.bang_sectioned_args simp_modifiers'; |
492 |
492 |
493 |
493 |
494 (* setup_methods *) |
494 (* setup_methods *) |
495 |
495 |