| changeset 23527 | c1d2fa4b76df |
| parent 23521 | 195fe3fe2831 |
| child 23544 | 4b4165cb3e0d |
--- a/src/HOL/Ring_and_Field.thy Mon Jul 02 23:14:06 2007 +0200 +++ b/src/HOL/Ring_and_Field.thy Tue Jul 03 01:26:06 2007 +0200 @@ -308,6 +308,8 @@ class pordered_comm_ring = comm_ring + pordered_comm_semiring +instance pordered_comm_ring \<subseteq> pordered_ring .. + instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring .. class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +