division ring assumes divide_inverse

--- a/src/HOL/NSA/StarDef.thy	Wed Feb 10 08:49:25 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy	Wed Feb 10 08:49:26 2010 +0100
@@ -893,6 +893,7 @@
 apply (intro_classes)
 apply (transfer, erule left_inverse)
 apply (transfer, erule right_inverse)
+apply (transfer, fact divide_inverse)
 done
 
 instance star :: (field) field

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