Inserted warning about defs with extra vars on rhs.
authornipkow
Fri Nov 24 09:27:19 1995 +0100 (1995-11-24)
changeset 13663f3c25d3ec04
parent 1365 0defae128e43
child 1367 78bdb2d04771
Inserted warning about defs with extra vars on rhs.
doc-src/Intro/advanced.tex
     1.1 --- a/doc-src/Intro/advanced.tex	Thu Nov 23 13:52:53 1995 +0100
     1.2 +++ b/doc-src/Intro/advanced.tex	Fri Nov 24 09:27:19 1995 +0100
     1.3 @@ -437,6 +437,19 @@
     1.4  end
     1.5  \end{ttbox}
     1.6  
     1.7 +\begin{warn}
     1.8 +A common mistake when writing definitions is to introduce extra free variables
     1.9 +on the right-hard side as in the following fictitious definition:
    1.10 +\begin{ttbox}
    1.11 +defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
    1.12 +\end{ttbox}
    1.13 +Isabelle rejects this ``definition'' because of the extra {\tt m} on the
    1.14 +right-hard side, which would introduce an inconsistency. What you should have
    1.15 +written is
    1.16 +\begin{ttbox}
    1.17 +defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"
    1.18 +\end{ttbox}
    1.19 +\end{warn}
    1.20  
    1.21  \subsection{Declaring type constructors}
    1.22  \indexbold{types!declaring}\indexbold{arities!declaring}