src/HOL/Lattices.thy
changeset 32063 2aab4f2af536
parent 31991 37390299214a
child 32064 53ca12ff305d
     1.1 --- a/src/HOL/Lattices.thy	Sun Jul 12 14:48:01 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Mon Jul 13 08:25:43 2009 +0200
     1.3 @@ -458,12 +458,6 @@
     1.4  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
     1.5    mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
     1.6  
     1.7 -text {*
     1.8 -  Now we have inherited antisymmetry as an intro-rule on all
     1.9 -  linear orders. This is a problem because it applies to bool, which is
    1.10 -  undesirable.
    1.11 -*}
    1.12 -
    1.13  lemmas [rule del] = min_max.le_infI min_max.le_supI
    1.14    min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
    1.15    min_max.le_infI1 min_max.le_infI2