# HG changeset patch # User nipkow # Date 823096946 -3600 # Node ID 3d19a5ddc21ef965a7b0603b2fba30d143591d3b # Parent bf18d174e9f814091e5e5f827f8a47c7b46e20ba Typo diff -r bf18d174e9f8 -r 3d19a5ddc21e doc-src/Intro/advanced.tex --- 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)"