src/HOL/Lattices_Big.thy
changeset 54857 5c05f7c5f8ae
parent 54745 46e441e61ff5
child 54863 82acc20ded73
     1.1 --- a/src/HOL/Lattices_Big.thy	Tue Dec 24 11:24:14 2013 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Tue Dec 24 11:24:16 2013 +0100
     1.3 @@ -373,12 +373,8 @@
     1.4  
     1.5  lemmas le_maxI1 = min_max.sup_ge1
     1.6  lemmas le_maxI2 = min_max.sup_ge2
     1.7 - 
     1.8 -lemmas min_ac = min_max.inf_assoc min_max.inf_commute
     1.9 -  min.left_commute
    1.10 -
    1.11 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute
    1.12 -  max.left_commute
    1.13 +lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
    1.14 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
    1.15  
    1.16  end
    1.17