# HG changeset patch
# User nipkow
# Date 823104903 -3600
# Node ID dcac709dcdd973f915d976d06e4be3f4f673e317
# Parent  3d19a5ddc21ef965a7b0603b2fba30d143591d3b
right-hard -> right-hand

diff -r 3d19a5ddc21e -r dcac709dcdd9 doc-src/Intro/advanced.tex
--- 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}