# HG changeset patch
# User huffman
# Date 1158262586 -7200
# Node ID 588ba06ba867e8a4ab7c15f3ba37d0bdacba76f2
# Parent  a7b2f90f698d1a0e6654efe6f63b94648ec3f0ea
add instance for class division_ring

diff -r a7b2f90f698d -r 588ba06ba867 src/HOL/Hyperreal/StarClasses.thy
--- 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)