--- a/src/HOL/NSA/StarDef.thy Tue Apr 27 08:17:39 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Tue Apr 27 08:17:40 2010 +0200
@@ -896,14 +896,19 @@
apply (transfer, fact divide_inverse)
done
+instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
+by (intro_classes, transfer, rule inverse_zero)
+
instance star :: (field) field
apply (intro_classes)
apply (transfer, erule left_inverse)
apply (transfer, rule divide_inverse)
done
-instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
-by (intro_classes, transfer, rule inverse_zero)
+instance star :: (field_inverse_zero) field_inverse_zero
+apply intro_classes
+apply (rule inverse_zero)
+done
instance star :: (ordered_semiring) ordered_semiring
apply (intro_classes)
@@ -945,6 +950,10 @@
instance star :: (linordered_idom) linordered_idom ..
instance star :: (linordered_field) linordered_field ..
+instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero
+apply intro_classes
+apply (rule inverse_zero)
+done
subsection {* Power *}