# HG changeset patch
# User kleing
# Date 1011451493 -3600
# Node ID e7b4c0731d57f3b043da0a38d83e0020f5e8328f
# Parent  fcbb6ad5c79093c5d7125d31884b9ac235a6eb6c
fixed typos

diff -r fcbb6ad5c790 -r e7b4c0731d57 src/HOL/Lattice/Lattice.thy
--- 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.
 *}