
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 \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70)
+  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70) where
   "x && y = (THE inf. is_inf x y inf)"
-  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65)
+definition
+  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65) where
   "x || y = (THE sup. is_sup x y sup)"
 
 notation (xsymbols)
-  meet  (infixl "\<sqinter>" 70)
+  meet  (infixl "\<sqinter>" 70) and
   join  (infixl "\<squnion>" 65)
 
 text {*
@@ -337,9 +338,10 @@
 *}
 
 definition
-  minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
+  minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
   "minimum x y = (if x \<sqsubseteq> y then x else y)"
-  maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
+definition
+  maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
   "maximum x y = (if x \<sqsubseteq> y then y else x)"
 
 lemma is_inf_minimum: "is_inf x y (minimum x y)"




