1.1 --- a/src/HOL/Complete_Lattice.thy Thu Aug 04 07:31:59 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Thu Aug 04 07:33:08 2011 +0200
1.3 @@ -405,7 +405,7 @@
1.4 apply (simp_all add: inf_Sup sup_Inf)*)
1.5
1.6 subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice}
1.7 - and proof @{text inf_Sup} and @{text sup_Inf} from that? *}
1.8 + and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
1.9 fix a b c
1.10 from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
1.11 then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)