src/HOL/Lattices.thy
changeset 24640 85a6c200ecd3
parent 24514 540eaf87e42d
child 24749 151b3758f576
     1.1 --- a/src/HOL/Lattices.thy	Tue Sep 18 18:51:07 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Sep 18 18:52:17 2007 +0200
     1.3 @@ -289,8 +289,7 @@
     1.4    fix x y z
     1.5    show "max x (min y z) = min (max x y) (max x z)"
     1.6    unfolding min_def max_def
     1.7 -    by (auto simp add: intro: antisym, unfold not_le,
     1.8 -      auto intro: less_trans le_less_trans aux)
     1.9 +  by auto
    1.10  qed (auto simp add: min_def max_def not_le less_imp_le)
    1.11  
    1.12  interpretation min_max: