# HG changeset patch
# User huffman
# Date 1183418766 -7200
# Node ID c1d2fa4b76dfe010e7e9ff65d749592632cb8f7c
# Parent  936dc616a7fba1c7b07b785392ee1b7237988106
instance pordered_comm_ring < pordered_ring

diff -r 936dc616a7fb -r c1d2fa4b76df src/HOL/Ring_and_Field.thy
--- 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 +