src/HOL/Ring_and_Field.thy
changeset 22452 8a86fd2a1bf0
parent 22422 ee19cdb07528
child 22548 6ce4bddf3bcb
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:07 2007 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:08 2007 +0100
     1.3 @@ -265,7 +265,7 @@
     1.4  
     1.5  instance pordered_ring \<subseteq> pordered_ab_group_add ..
     1.6  
     1.7 -axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
     1.8 +class lordered_ring = pordered_ring + lordered_ab_group_abs
     1.9  
    1.10  instance lordered_ring \<subseteq> lordered_ab_group_meet ..
    1.11  
    1.12 @@ -274,9 +274,7 @@
    1.13  class abs_if = minus + ord + zero +
    1.14    assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
    1.15  
    1.16 -class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
    1.17 -
    1.18 -instance ordered_ring_strict \<subseteq> lordered_ab_group ..
    1.19 +class ordered_ring_strict = ring + ordered_semiring_strict + abs_if + lordered_ab_group
    1.20  
    1.21  instance ordered_ring_strict \<subseteq> lordered_ring
    1.22    by intro_classes (simp add: abs_if sup_eq_if)
    1.23 @@ -287,7 +285,7 @@
    1.24    (*previously ordered_semiring*)
    1.25    assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
    1.26  
    1.27 -class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
    1.28 +class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if + lordered_ab_group
    1.29    (*previously ordered_ring*)
    1.30  
    1.31  instance ordered_idom \<subseteq> ordered_ring_strict ..