--- a/src/HOL/Ring_and_Field.thy Tue May 22 14:43:54 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Tue May 22 16:47:22 2007 +0200
@@ -287,6 +287,8 @@
class pordered_comm_ring = comm_ring + pordered_comm_semiring
+instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring ..
+
class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
(*previously ordered_semiring*)
assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
@@ -296,6 +298,8 @@
instance ordered_idom \<subseteq> ordered_ring_strict ..
+instance ordered_idom \<subseteq> pordered_comm_ring ..
+
class ordered_field = field + ordered_idom
lemmas linorder_neqE_ordered_idom =