--- a/src/HOL/Lattice/Lattice.thy Fri Jan 18 18:36:19 2002 +0100
+++ b/src/HOL/Lattice/Lattice.thy Sat Jan 19 15:44:53 2002 +0100
@@ -150,7 +150,7 @@
subsection {* Algebraic properties \label{sec:lattice-algebra} *}
text {*
- The @{text \<sqinter>} and @{text \<squnion>} operations have to following
+ The @{text \<sqinter>} and @{text \<squnion>} operations have the following
characteristic algebraic properties: associative (A), commutative
(C), and absorptive (AB).
*}
@@ -332,7 +332,7 @@
subsubsection {* Linear orders *}
text {*
- Linear orders with @{term minimum} and @{term minimum} operations
+ Linear orders with @{term minimum} and @{term maximum} operations
are a (degenerate) example of lattice structures.
*}