src/HOL/Lattices.thy
changeset 23018 1d29bc31b0cb
parent 22916 8caf6da610e2
child 23087 ad7244663431
     1.1 --- a/src/HOL/Lattices.thy	Sat May 19 11:33:21 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Sat May 19 11:33:22 2007 +0200
     1.3 @@ -282,7 +282,7 @@
     1.4    special case of @{const inf}/@{const sup} *}
     1.5  
     1.6  lemma (in linorder) distrib_lattice_min_max:
     1.7 -  "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
     1.8 +  "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
     1.9  proof unfold_locales
    1.10    have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
    1.11      by (auto simp add: less_le antisym)