src/HOL/Int.thy
changeset 55911 d00023bd3554
parent 55404 5cb95b79a51f
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Int.thy	Tue Mar 04 14:14:28 2014 -0800
     1.2 +++ b/src/HOL/Int.thy	Tue Mar 04 15:26:12 2014 -0800
     1.3 @@ -766,13 +766,6 @@
     1.4    {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
     1.5  
     1.6  
     1.7 -subsection{*Lemmas About Small Numerals*}
     1.8 -
     1.9 -lemma abs_power_minus_one [simp]:
    1.10 -  "abs(-1 ^ n) = (1::'a::linordered_idom)"
    1.11 -by (simp add: power_abs)
    1.12 -
    1.13 -
    1.14  subsection{*More Inequality Reasoning*}
    1.15  
    1.16  lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
    1.17 @@ -1226,9 +1219,6 @@
    1.18    unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
    1.19    by simp
    1.20  
    1.21 -lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
    1.22 -  by (fact divide_minus_left)
    1.23 -
    1.24  lemma half_gt_zero_iff:
    1.25    "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
    1.26    by auto