equal
deleted
inserted
replaced
900 apply (intro_classes) |
900 apply (intro_classes) |
901 apply (transfer, erule left_inverse) |
901 apply (transfer, erule left_inverse) |
902 apply (transfer, rule divide_inverse) |
902 apply (transfer, rule divide_inverse) |
903 done |
903 done |
904 |
904 |
905 instance star :: (division_by_zero) division_by_zero |
905 instance star :: (division_ring_inverse_zero) division_ring_inverse_zero |
906 by (intro_classes, transfer, rule inverse_zero) |
906 by (intro_classes, transfer, rule inverse_zero) |
907 |
907 |
908 instance star :: (ordered_semiring) ordered_semiring |
908 instance star :: (ordered_semiring) ordered_semiring |
909 apply (intro_classes) |
909 apply (intro_classes) |
910 apply (transfer, erule (1) mult_left_mono) |
910 apply (transfer, erule (1) mult_left_mono) |