| changeset 21896 | 9a7949815a84 |
| parent 21657 | 2a0c0fa4a3c4 |
| child 22063 | 717425609192 |
--- a/src/HOL/Algebra/Lattice.thy Thu Dec 21 13:55:15 2006 +0100 +++ b/src/HOL/Algebra/Lattice.thy Fri Dec 22 14:03:30 2006 +0100 @@ -34,7 +34,7 @@ text {* Upper and lower bounds of a set. *} definition (in order_syntax) - Upper where + Upper :: "'a set => 'a set" where "Upper A == {u. (ALL x. x \<in> A \<inter> L --> x \<sqsubseteq> u)} \<inter> L" definition (in order_syntax)