--- a/doc-src/Intro/advanced.tex Tue Jan 30 15:31:04 1996 +0100
+++ b/doc-src/Intro/advanced.tex Wed Jan 31 15:02:26 1996 +0100
@@ -445,7 +445,7 @@
defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
\end{ttbox}
Isabelle rejects this ``definition'' because of the extra {\tt m} on the
-right-hard side, which would introduce an inconsistency. What you should have
+right-hand side, which would introduce an inconsistency. What you should have
written is
\begin{ttbox}
defs prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"