# HG changeset patch
# User huffman
# Date 1179845242 -7200
# Node ID d810dc04b96d30e1b82fdbf3cb89cd769fd62bc8
# Parent  f64df9399329c66b1a80952a14efe95672fbe090
add missing instance declarations

diff -r f64df9399329 -r d810dc04b96d src/HOL/Ring_and_Field.thy
--- 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 =