src/HOL/Presburger.thy
changeset 26075 815f3ccc0b45
parent 25919 8b1c0d434824
child 26086 3c243098b64a
     1.1 --- a/src/HOL/Presburger.thy	Fri Feb 15 23:22:02 2008 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Sat Feb 16 02:01:13 2008 +0100
     1.3 @@ -671,20 +671,19 @@
     1.4    unfolding number_of_is_id ..
     1.5  
     1.6  lemmas pred_succ_numeral_code [code func] =
     1.7 -  arith_simps(5-12)
     1.8 +  pred_bin_simps succ_bin_simps
     1.9  
    1.10  lemmas plus_numeral_code [code func] =
    1.11 -  arith_simps(13-17)
    1.12 -  arith_simps(26-27)
    1.13 +  add_bin_simps
    1.14    arith_extra_simps(1) [where 'a = int]
    1.15  
    1.16  lemmas minus_numeral_code [code func] =
    1.17 -  arith_simps(18-21)
    1.18 +  minus_bin_simps
    1.19    arith_extra_simps(2) [where 'a = int]
    1.20    arith_extra_simps(5) [where 'a = int]
    1.21  
    1.22  lemmas times_numeral_code [code func] =
    1.23 -  arith_simps(22-25)
    1.24 +  mult_bin_simps
    1.25    arith_extra_simps(4) [where 'a = int]
    1.26  
    1.27  lemmas eq_numeral_code [code func] =