| changeset 20540 | 588ba06ba867 |
| parent 17429 | e8d6ed3aacfe |
| child 20553 | 7ced6152e52c |
--- 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)