ignore_neq also influences arith_tac now, not just fast_arith_tac
authornipkow
Fri Apr 02 12:25:48 2004 +0200 (2004-04-02)
changeset 145070af3da3beae8
parent 14506 6807f524ac4d
child 14508 859b11514537
ignore_neq also influences arith_tac now, not just fast_arith_tac
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/arith_data.ML	Fri Apr 02 12:08:38 2004 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Fri Apr 02 12:25:48 2004 +0200
     1.3 @@ -435,10 +435,14 @@
     1.4  local
     1.5  
     1.6  fun raw_arith_tac ex i st =
     1.7 +  let fun elim_neq_tac i =
     1.8 +      COND (K(!ignore_neq)) all_tac (REPEAT_DETERM(etac linorder_neqE i))
     1.9 +  in
    1.10    refute_tac (K true)
    1.11     (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
    1.12 -   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
    1.13 -   i st;
    1.14 +   (elim_neq_tac THEN' fast_ex_arith_tac ex)
    1.15 +   i st
    1.16 +  end;
    1.17  
    1.18  fun presburger_tac i st =
    1.19    (case ArithTheoryData.get_sg (sign_of_thm st) of