got rid of ignore_neq again.
authornipkow
Fri Apr 02 14:47:11 2004 +0200 (2004-04-02)
changeset 145099d8978a2ae56
parent 14508 859b11514537
child 14510 73ea1234bb23
got rid of ignore_neq again.
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/arith_data.ML	Fri Apr 02 14:08:30 2004 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Fri Apr 02 14:47:11 2004 +0200
     1.3 @@ -231,12 +231,6 @@
     1.4    {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
     1.5  
     1.6  
     1.7 -(* A FIXME to avoid excessive case splits when ~= is split into < and >:
     1.8 -   ignore ~= altogether.
     1.9 -*)
    1.10 -
    1.11 -val ignore_neq = ref false;
    1.12 -
    1.13  structure LA_Data_Ref: LIN_ARITH_DATA =
    1.14  struct
    1.15  
    1.16 @@ -339,8 +333,7 @@
    1.17       | _       => None
    1.18    end handle Zero => None;
    1.19  
    1.20 -fun negate(Some(x,i,rel,y,j,d)) =
    1.21 -      if rel = "=" andalso !ignore_neq then None else Some(x,i,"~"^rel,y,j,d)
    1.22 +fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
    1.23    | negate None = None;
    1.24  
    1.25  fun decomp1 (discrete,inj_consts) (T,xxx) =
    1.26 @@ -435,14 +428,10 @@
    1.27  local
    1.28  
    1.29  fun raw_arith_tac ex i st =
    1.30 -  let fun elim_neq_tac i =
    1.31 -      COND (K(!ignore_neq)) all_tac (REPEAT_DETERM(etac linorder_neqE i))
    1.32 -  in
    1.33    refute_tac (K true)
    1.34     (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
    1.35 -   (elim_neq_tac THEN' fast_ex_arith_tac ex)
    1.36 -   i st
    1.37 -  end;
    1.38 +   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
    1.39 +   i st;
    1.40  
    1.41  fun presburger_tac i st =
    1.42    (case ArithTheoryData.get_sg (sign_of_thm st) of