instance pordered_comm_ring < pordered_ring

--- 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 +