src/HOL/Tools/int_arith.ML
changeset 31024 0fdf666e08bf
parent 30802 f9e9e800d27e
child 31068 f591144b0f17
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Apr 29 13:36:29 2009 -0700
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Apr 29 17:15:01 2009 -0700
     1.3 @@ -6,27 +6,6 @@
     1.4  structure Int_Numeral_Simprocs =
     1.5  struct
     1.6  
     1.7 -(*reorientation simprules using ==, for the following simproc*)
     1.8 -val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
     1.9 -val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    1.10 -val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    1.11 -
    1.12 -(*reorientation simplification procedure: reorients (polymorphic) 
    1.13 -  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    1.14 -fun reorient_proc sg _ (_ $ t $ u) =
    1.15 -  case u of
    1.16 -      Const(@{const_name HOL.zero}, _) => NONE
    1.17 -    | Const(@{const_name HOL.one}, _) => NONE
    1.18 -    | Const(@{const_name Int.number_of}, _) $ _ => NONE
    1.19 -    | _ => SOME (case t of
    1.20 -        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    1.21 -      | Const(@{const_name HOL.one}, _) => meta_one_reorient
    1.22 -      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    1.23 -
    1.24 -val reorient_simproc = 
    1.25 -  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
    1.26 -
    1.27 -
    1.28  (** Utilities **)
    1.29  
    1.30  fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
    1.31 @@ -383,7 +362,6 @@
    1.32  
    1.33  end;
    1.34  
    1.35 -Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
    1.36  Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
    1.37  Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
    1.38  Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];