src/HOL/Ring_and_Field.thy
changeset 22422 ee19cdb07528
parent 22390 378f34b1e380
child 22452 8a86fd2a1bf0
     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -279,7 +279,7 @@
     1.4  instance ordered_ring_strict \<subseteq> lordered_ab_group ..
     1.5  
     1.6  instance ordered_ring_strict \<subseteq> lordered_ring
     1.7 -  by (intro_classes, simp add: abs_if join_eq_if)
     1.8 +  by intro_classes (simp add: abs_if sup_eq_if)
     1.9  
    1.10  class pordered_comm_ring = comm_ring + pordered_comm_semiring
    1.11