src/HOL/Lattices.thy
changeset 28823 dcbef866c9e2
parent 28692 a2bc5ce0c9fc
child 29223 e09c53289830
     1.1 --- a/src/HOL/Lattices.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -291,7 +291,7 @@
     1.4  
     1.5  lemma (in linorder) distrib_lattice_min_max:
     1.6    "distrib_lattice (op \<le>) (op <) min max"
     1.7 -proof unfold_locales
     1.8 +proof
     1.9    have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    1.10      by (auto simp add: less_le antisym)
    1.11    fix x y z