--- a/src/HOL/Numeral_Simprocs.thy Sun Oct 30 07:08:33 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Sun Oct 30 09:07:02 2011 +0100
@@ -113,7 +113,9 @@
|"(l::'a::number_ring) - m = n"
|"(l::'a::number_ring) = m - n"
|"(l::'a::number_ring) * m = n"
- |"(l::'a::number_ring) = m * n") =
+ |"(l::'a::number_ring) = m * n"
+ |"- (l::'a::number_ring) = m"
+ |"(l::'a::number_ring) = - m") =
{* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
simproc_setup intless_cancel_numerals
@@ -122,7 +124,9 @@
|"(l::'a::{linordered_idom,number_ring}) - m < n"
|"(l::'a::{linordered_idom,number_ring}) < m - n"
|"(l::'a::{linordered_idom,number_ring}) * m < n"
- |"(l::'a::{linordered_idom,number_ring}) < m * n") =
+ |"(l::'a::{linordered_idom,number_ring}) < m * n"
+ |"- (l::'a::{linordered_idom,number_ring}) < m"
+ |"(l::'a::{linordered_idom,number_ring}) < - m") =
{* fn phi => Numeral_Simprocs.less_cancel_numerals *}
simproc_setup intle_cancel_numerals
@@ -131,7 +135,9 @@
|"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
|"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
|"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
- |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") =
+ |"(l::'a::{linordered_idom,number_ring}) \<le> m * n"
+ |"- (l::'a::{linordered_idom,number_ring}) \<le> m"
+ |"(l::'a::{linordered_idom,number_ring}) \<le> - m") =
{* fn phi => Numeral_Simprocs.le_cancel_numerals *}
simproc_setup ring_eq_cancel_numeral_factor