right-hard -> right-hand
authornipkow
Wed Jan 31 17:15:03 1996 +0100 (1996-01-31)
changeset 1468dcac709dcdd9
parent 1467 3d19a5ddc21e
child 1469 fb9ccf06dfe8
right-hard -> right-hand
doc-src/Intro/advanced.tex
     1.1 --- a/doc-src/Intro/advanced.tex	Wed Jan 31 15:02:26 1996 +0100
     1.2 +++ b/doc-src/Intro/advanced.tex	Wed Jan 31 17:15:03 1996 +0100
     1.3 @@ -421,7 +421,7 @@
     1.4  \indexbold{definitions} The {\bf definition part} is similar, but with the
     1.5  keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are rules of the
     1.6  form $t\equiv u$, and should serve only as abbreviations.  Isabelle checks for
     1.7 -common errors in definitions, such as extra variables on the right-hard side.
     1.8 +common errors in definitions, such as extra variables on the right-hand side.
     1.9  Determined users can write non-conservative `definitions' by using mutual
    1.10  recursion, for example; the consequences of such actions are their
    1.11  responsibility.
    1.12 @@ -440,7 +440,7 @@
    1.13  
    1.14  \begin{warn}
    1.15  A common mistake when writing definitions is to introduce extra free variables
    1.16 -on the right-hard side as in the following fictitious definition:
    1.17 +on the right-hand side as in the following fictitious definition:
    1.18  \begin{ttbox}
    1.19  defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
    1.20  \end{ttbox}