src/HOL/Lattices_Big.thy
changeset 54863 82acc20ded73
parent 54857 5c05f7c5f8ae
child 54864 a064732223ad
     1.1 --- a/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -371,10 +371,10 @@
     1.4      by (simp only: min_max.Sup_fin_def Max_def)
     1.5  qed
     1.6  
     1.7 -lemmas le_maxI1 = min_max.sup_ge1
     1.8 -lemmas le_maxI2 = min_max.sup_ge2
     1.9 -lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
    1.10 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
    1.11 +lemmas le_maxI1 = max.cobounded1
    1.12 +lemmas le_maxI2 = max.cobounded2
    1.13 +lemmas min_ac = min.assoc min.commute min.left_commute
    1.14 +lemmas max_ac = max.assoc max.commute max.left_commute
    1.15  
    1.16  end
    1.17