diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Lattice/Lattice.thy Fri Nov 17 02:20:03 2006 +0100 @@ -25,13 +25,14 @@ *} definition - meet :: "'a::lattice \ 'a \ 'a" (infixl "&&" 70) + meet :: "'a::lattice \ 'a \ 'a" (infixl "&&" 70) where "x && y = (THE inf. is_inf x y inf)" - join :: "'a::lattice \ 'a \ 'a" (infixl "||" 65) +definition + join :: "'a::lattice \ 'a \ 'a" (infixl "||" 65) where "x || y = (THE sup. is_sup x y sup)" notation (xsymbols) - meet (infixl "\" 70) + meet (infixl "\" 70) and join (infixl "\" 65) text {* @@ -337,9 +338,10 @@ *} definition - minimum :: "'a::linear_order \ 'a \ 'a" + minimum :: "'a::linear_order \ 'a \ 'a" where "minimum x y = (if x \ y then x else y)" - maximum :: "'a::linear_order \ 'a \ 'a" +definition + maximum :: "'a::linear_order \ 'a \ 'a" where "maximum x y = (if x \ y then y else x)" lemma is_inf_minimum: "is_inf x y (minimum x y)"