diff -r 89c54f51f55a -r 39be26d1bc28 src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Apr 26 11:34:15 2010 +0200 +++ b/src/HOL/Int.thy Mon Apr 26 11:34:17 2010 +0200 @@ -1995,15 +1995,15 @@ text{*Division By @{text "-1"}*} lemma divide_minus1 [simp]: - "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" + "x/-1 = -(x::'a::{field,division_ring_inverse_zero,number_ring})" by simp lemma minus1_divide [simp]: - "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" + "-1 / (x::'a::{field,division_ring_inverse_zero,number_ring}) = - (1/x)" by (simp add: divide_inverse) lemma half_gt_zero_iff: - "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))" + "(0 < r/2) = (0 < (r::'a::{linordered_field,division_ring_inverse_zero,number_ring}))" by auto lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]