--- a/src/HOL/Isar_examples/KnasterTarski.thy Wed Oct 13 19:44:33 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Thu Oct 14 01:07:24 1999 +0200
@@ -15,7 +15,7 @@
text {*
According to the book ``Introduction to Lattices and Order''
\cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint
- theorem is as follows.\footnote{We have dualized their argument, and
+ theorem is as follows.\footnote{We have dualized the argument, and
tuned the notation a little bit.}
\medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a