--- a/src/HOL/Rings.thy Wed Feb 10 08:49:25 2010 +0100
+++ b/src/HOL/Rings.thy Wed Feb 10 08:49:26 2010 +0100
@@ -410,9 +410,14 @@
end
+class inverse =
+ fixes inverse :: "'a \<Rightarrow> 'a"
+ and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+
class division_ring = ring_1 + inverse +
assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
+ assumes divide_inverse: "a / b = a * inverse b"
begin
subclass ring_1_no_zero_divisors