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