src/HOL/Tools/int_arith.ML
changeset 30732 afca5be252d6
parent 30685 dd5fe091ff04
child 30802 f9e9e800d27e
     1.1 --- a/src/HOL/Tools/int_arith.ML	Thu Mar 26 14:30:20 2009 +0000
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Mar 26 11:33:50 2009 -0700
     1.3 @@ -377,6 +377,8 @@
     1.4  struct
     1.5    val assoc_ss = HOL_ss addsimps @{thms mult_ac}
     1.6    val eq_reflection = eq_reflection
     1.7 +  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
     1.8 +    | is_numeral _ = false;
     1.9  end;
    1.10  
    1.11  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);