diff -r 6c0702a96076 -r ce5daf09ebfe src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Tue Jan 09 18:12:59 2007 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Tue Jan 09 18:13:55 2007 +0100
@@ -239,7 +239,7 @@
 declare inverse_eq_divide_number_of [simp]
 
 
-text{*These laws simplify inequalities, moving unary minus from a term
+subsubsection{*These laws simplify inequalities, moving unary minus from a term
 into the literal.*}
 lemmas less_minus_iff_number_of =
     less_minus_iff [of "number_of v", standard]
@@ -267,27 +267,40 @@
 declare minus_equation_iff_number_of [simp]
 
 
-text{*These simplify inequalities where one side is the constant 1.*}
-lemmas less_minus_iff_1 = less_minus_iff [of 1, simplified]
-declare less_minus_iff_1 [simp]
+subsubsection{*To Simplify Inequalities Where One Side is the Constant 1*}
 
-lemmas le_minus_iff_1 = le_minus_iff [of 1, simplified]
-declare le_minus_iff_1 [simp]
+lemma less_minus_iff_1 [simp]: 
+  fixes b::"'b::{ordered_idom,number_ring}" 
+  shows "(1 < - b) = (b < -1)"
+by auto
+
+lemma le_minus_iff_1 [simp]: 
+  fixes b::"'b::{ordered_idom,number_ring}" 
+  shows "(1 \<le> - b) = (b \<le> -1)"
+by auto
 
-lemmas equation_minus_iff_1 = equation_minus_iff [of 1, simplified]
-declare equation_minus_iff_1 [simp]
+lemma equation_minus_iff_1 [simp]: 
+  fixes b::"'b::number_ring" 
+  shows "(1 = - b) = (b = -1)"
+by (subst equation_minus_iff, auto) 
 
-lemmas minus_less_iff_1 = minus_less_iff [of _ 1, simplified]
-declare minus_less_iff_1 [simp]
+lemma minus_less_iff_1 [simp]: 
+  fixes a::"'b::{ordered_idom,number_ring}" 
+  shows "(- a < 1) = (-1 < a)"
+by auto
 
-lemmas minus_le_iff_1 = minus_le_iff [of _ 1, simplified]
-declare minus_le_iff_1 [simp]
+lemma minus_le_iff_1 [simp]: 
+  fixes a::"'b::{ordered_idom,number_ring}" 
+  shows "(- a \<le> 1) = (-1 \<le> a)"
+by auto
 
-lemmas minus_equation_iff_1 = minus_equation_iff [of _ 1, simplified]
-declare minus_equation_iff_1 [simp]
+lemma minus_equation_iff_1 [simp]: 
+  fixes a::"'b::number_ring" 
+  shows "(- a = 1) = (a = -1)"
+by (subst minus_equation_iff, auto) 
 
 
-text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
+subsubsection {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
 
 lemmas mult_less_cancel_left_number_of =
     mult_less_cancel_left [of "number_of v", standard]
@@ -306,7 +319,7 @@
 declare mult_le_cancel_right_number_of [simp]
 
 
-text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
+subsubsection {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
 
 lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard]
 declare le_divide_eq_number_of [simp]