# HG changeset patch
# User haftmann
# Date 1265788166 -3600
# Node ID 3246e66b08749f2cb88ae62ba40e99077b95743b
# Parent  96a21dd3b34929d706b0dfbb6ad21e0cad6f9c54
division ring assumes divide_inverse

diff -r 96a21dd3b349 -r 3246e66b0874 src/HOL/NSA/StarDef.thy
--- 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
diff -r 96a21dd3b349 -r 3246e66b0874 src/HOL/Rings.thy
--- 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