add missing instance declarations
authorhuffman
Tue May 22 16:47:22 2007 +0200 (2007-05-22)
changeset 23073d810dc04b96d
parent 23072 f64df9399329
child 23074 a53cb8ddb052
add missing instance declarations
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue May 22 14:43:54 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue May 22 16:47:22 2007 +0200
     1.3 @@ -287,6 +287,8 @@
     1.4  
     1.5  class pordered_comm_ring = comm_ring + pordered_comm_semiring
     1.6  
     1.7 +instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring ..
     1.8 +
     1.9  class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
    1.10    (*previously ordered_semiring*)
    1.11    assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
    1.12 @@ -296,6 +298,8 @@
    1.13  
    1.14  instance ordered_idom \<subseteq> ordered_ring_strict ..
    1.15  
    1.16 +instance ordered_idom \<subseteq> pordered_comm_ring ..
    1.17 +
    1.18  class ordered_field = field + ordered_idom
    1.19  
    1.20  lemmas linorder_neqE_ordered_idom =