add instance for class division_ring

--- a/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 14 20:31:10 2006 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 14 21:36:26 2006 +0200
@@ -300,6 +300,12 @@
 instance star :: (comm_ring_1) comm_ring_1 ..
 instance star :: (idom) idom .. 
 
+instance star :: (division_ring) division_ring
+apply (intro_classes)
+apply (transfer, erule left_inverse)
+apply (transfer, erule right_inverse)
+done
+
 instance star :: (field) field
 apply (intro_classes)
 apply (transfer, erule left_inverse)