--- 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]