--- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Feb 16 08:27:17 2001 +0100
@@ -74,7 +74,7 @@
\end{isabelle}
This may be viewed as a fixed point finder or as one half of the well known
\emph{Union-Find} algorithm.
-The snag is that it may not terminate if \isa{f} has nontrivial cycles.
+The snag is that it may not terminate if \isa{f} has non-trivial cycles.
Phrased differently, the relation%
\end{isamarkuptext}%
\isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline