src/HOL/arith_data.ML
changeset 10516 dc113303d101
parent 9893 93d2fde0306c
child 10574 8f98f0301d67
     1.1 --- a/src/HOL/arith_data.ML	Thu Nov 23 21:29:50 2000 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Thu Nov 23 21:33:14 2000 +0100
     1.3 @@ -406,13 +406,23 @@
     1.4     (max m n + k <= r) = (m+k <= r & n+k <= r)
     1.5     (l <= min m n + k) = (l <= m+k & l <= n+k)
     1.6  *)
     1.7 -fun arith_tac i st =
     1.8 +local
     1.9 +
    1.10 +val atomize_tac = Method.atomize_tac (thms "atomize'");
    1.11 +
    1.12 +fun raw_arith_tac i st =
    1.13    refute_tac (K true) (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
    1.14               ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
    1.15  
    1.16 +in
    1.17 +
    1.18 +val arith_tac = atomize_tac THEN' raw_arith_tac;
    1.19 +
    1.20  fun arith_method prems =
    1.21    Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
    1.22  
    1.23 +end;
    1.24 +
    1.25  
    1.26  (* theory setup *)
    1.27