src/HOL/Numeral_Simprocs.thy
changeset 55375 d26d5f988d71
parent 54489 03ff4d1e6784
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Feb 09 13:07:23 2014 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Feb 10 21:50:50 2014 +0100
     1.3 @@ -285,7 +285,8 @@
     1.4         @{simproc int_combine_numerals},
     1.5         @{simproc inteq_cancel_numerals},
     1.6         @{simproc intless_cancel_numerals},
     1.7 -       @{simproc intle_cancel_numerals}]
     1.8 +       @{simproc intle_cancel_numerals},
     1.9 +       @{simproc field_combine_numerals}]
    1.10    #> Lin_Arith.add_simprocs
    1.11        [@{simproc nat_combine_numerals},
    1.12         @{simproc nateq_cancel_numerals},