| changeset 36414 | a19ba9bbc8dc |
| parent 36412 | 9245942dcc5b |
| child 37765 | 26bdfb7b680b |
--- a/src/HOL/NSA/StarDef.thy Tue Apr 27 08:18:25 2010 +0200 +++ b/src/HOL/NSA/StarDef.thy Tue Apr 27 09:49:36 2010 +0200 @@ -950,10 +950,7 @@ 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 +instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero .. subsection {* Power *}