# HG changeset patch
# User haftmann
# Date 1247466343 -7200
# Node ID 2aab4f2af536367976cfb4a923a7d0a68ee2e148
# Parent  8f37cf60b8852a6f5f1b8dd1885db667860d250e
removed outdated comment

diff -r 8f37cf60b885 -r 2aab4f2af536 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Jul 12 14:48:01 2009 +0200
+++ b/src/HOL/Lattices.thy	Mon Jul 13 08:25:43 2009 +0200
@@ -458,12 +458,6 @@
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
 
-text {*
-  Now we have inherited antisymmetry as an intro-rule on all
-  linear orders. This is a problem because it applies to bool, which is
-  undesirable.
-*}
-
 lemmas [rule del] = min_max.le_infI min_max.le_supI
   min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
   min_max.le_infI1 min_max.le_infI2