author nipkow Wed, 31 Jan 1996 17:15:03 +0100 changeset 1468 dcac709dcdd9 parent 1467 3d19a5ddc21e child 1469 fb9ccf06dfe8
right-hard -> right-hand
--- a/doc-src/Intro/advanced.tex	Wed Jan 31 15:02:26 1996 +0100
+++ b/doc-src/Intro/advanced.tex	Wed Jan 31 17:15:03 1996 +0100
@@ -421,7 +421,7 @@
\indexbold{definitions} The {\bf definition part} is similar, but with the
keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are rules of the
form $t\equiv u$, and should serve only as abbreviations.  Isabelle checks for
-common errors in definitions, such as extra variables on the right-hard side.
+common errors in definitions, such as extra variables on the right-hand side.
Determined users can write non-conservative definitions' by using mutual
recursion, for example; the consequences of such actions are their
responsibility.
@@ -440,7 +440,7 @@

\begin{warn}
A common mistake when writing definitions is to introduce extra free variables
-on the right-hard side as in the following fictitious definition:
+on the right-hand side as in the following fictitious definition:
\begin{ttbox}
defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
\end{ttbox}`