Typo
authornipkow
Wed Jan 31 15:02:26 1996 +0100 (1996-01-31)
changeset 14673d19a5ddc21e
parent 1466 bf18d174e9f8
child 1468 dcac709dcdd9
Typo
doc-src/Intro/advanced.tex
     1.1 --- a/doc-src/Intro/advanced.tex	Tue Jan 30 15:31:04 1996 +0100
     1.2 +++ b/doc-src/Intro/advanced.tex	Wed Jan 31 15:02:26 1996 +0100
     1.3 @@ -445,7 +445,7 @@
     1.4  defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
     1.5  \end{ttbox}
     1.6  Isabelle rejects this ``definition'' because of the extra {\tt m} on the
     1.7 -right-hard side, which would introduce an inconsistency. What you should have
     1.8 +right-hand side, which would introduce an inconsistency. What you should have
     1.9  written is
    1.10  \begin{ttbox}
    1.11  defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"