changeset 23393 | 31781b2de73d |
parent 23373 | ead82c82da9e |
child 25469 | f81b3be9dfdd |
--- a/src/HOL/Lattice/Lattice.thy Thu Jun 14 22:59:42 2007 +0200 +++ b/src/HOL/Lattice/Lattice.thy Thu Jun 14 23:04:36 2007 +0200 @@ -232,7 +232,7 @@ show "x \<sqsubseteq> x" .. show "x \<sqsubseteq> x \<squnion> y" .. fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y" - show "z \<sqsubseteq> x" by assumption + show "z \<sqsubseteq> x" by fact qed theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"