--- a/src/HOL/Ring_and_Field.thy Mon Oct 04 15:25:28 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy Mon Oct 04 15:28:03 2004 +0200
@@ -580,12 +580,16 @@
lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
by (simp add: divide_inverse)
-lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
+lemma divide_self: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
by (simp add: divide_inverse)
lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
by (simp add: divide_inverse)
+lemma divide_self_if [simp]:
+ "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
+ by (simp add: divide_self)
+
lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
by (simp add: divide_inverse)