src/HOL/Integ/NatBin.thy
changeset 18708 4b3dadb4fe33
parent 18702 7dc7dcd63224
child 18978 8971c306b94f
     1.1 --- a/src/HOL/Integ/NatBin.thy	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -591,14 +591,14 @@
     1.4  val numeral_ss = simpset() addsimps numerals;
     1.5  
     1.6  val nat_bin_arith_setup =
     1.7 - [Fast_Arith.map_data 
     1.8 + Fast_Arith.map_data
     1.9     (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.10       {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    1.11        inj_thms = inj_thms,
    1.12        lessD = lessD, neqE = neqE,
    1.13        simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
    1.14                                    not_neg_number_of_Pls,
    1.15 -                                  neg_number_of_Min,neg_number_of_BIT]})]
    1.16 +                                  neg_number_of_Min,neg_number_of_BIT]})
    1.17  *}
    1.18  
    1.19  setup nat_bin_arith_setup