--- a/src/HOL/Int.thy Tue Mar 04 14:14:28 2014 -0800
+++ b/src/HOL/Int.thy Tue Mar 04 15:26:12 2014 -0800
@@ -766,13 +766,6 @@
{* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
-subsection{*Lemmas About Small Numerals*}
-
-lemma abs_power_minus_one [simp]:
- "abs(-1 ^ n) = (1::'a::linordered_idom)"
-by (simp add: power_abs)
-
-
subsection{*More Inequality Reasoning*}
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
@@ -1226,9 +1219,6 @@
unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
by simp
-lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
- by (fact divide_minus_left)
-
lemma half_gt_zero_iff:
"(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
by auto