src/HOL/Int.thy
changeset 58512 dc4d76dfa8f0
parent 57514 bdc2c6b40bf2
child 58649 a62065b5e1e2
     1.1 --- a/src/HOL/Int.thy	Thu Oct 02 11:33:05 2014 +0200
     1.2 +++ b/src/HOL/Int.thy	Thu Oct 02 11:33:06 2014 +0200
     1.3 @@ -1217,21 +1217,6 @@
     1.4    divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
     1.5    le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
     1.6  
     1.7 -text{*Division By @{text "-1"}*}
     1.8 -
     1.9 -lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
    1.10 -  unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
    1.11 -  by simp
    1.12 -
    1.13 -lemma half_gt_zero_iff:
    1.14 -  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
    1.15 -  by auto
    1.16 -
    1.17 -lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
    1.18 -
    1.19 -lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
    1.20 -  by (fact divide_numeral_1)
    1.21 -
    1.22  
    1.23  subsection {* The divides relation *}
    1.24