equal
deleted
inserted
replaced
912 ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, |
912 ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, |
913 more_arith_tacs ctxt]; |
913 more_arith_tacs ctxt]; |
914 |
914 |
915 fun arith_method src = |
915 fun arith_method src = |
916 Method.syntax Args.bang_facts src |
916 Method.syntax Args.bang_facts src |
917 #> (fn (prems, ctxt) => Method.METHOD (fn facts => |
917 #> (fn (prems, ctxt) => METHOD (fn facts => |
918 HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts) |
918 HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts) |
919 THEN' arith_tac ctxt))); |
919 THEN' arith_tac ctxt))); |
920 |
920 |
921 end; |
921 end; |
922 |
922 |