# HG changeset patch
# User nipkow
# Date 828633686 -7200
# Node ID c4901f7161c587ff570d581e91a9160564a1ea3c
# Parent  60ded8c1748cecb1ccda02a32ddb15f027af549e
Added 'constdefs' and extended the section on 'defs'

diff -r 60ded8c1748c -r c4901f7161c5 doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Thu Apr 04 17:31:37 1996 +0200
+++ b/doc-src/Intro/advanced.tex	Thu Apr 04 18:01:26 1996 +0200
@@ -420,12 +420,17 @@
 
 \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-hand side.
-Determined users can write non-conservative `definitions' by using mutual
-recursion, for example; the consequences of such actions are their
-responsibility.
-
+form $s \equiv t$, and should serve only as abbreviations. The simplest form
+of a definition is $f \equiv t$, where $f$ is a constant. Isabelle also
+allows a derived form where the parameters of $f$ appear on the left:
+\begin{itemize}
+\item In uncurried syntax: $f(x@1,\dots,x@n) \equiv u$ (\FOL, \ZF, \dots)
+\item In curried syntax: $f~x@1~\dots~x@n \equiv u$ (\HOL, \HOLCF)
+\end{itemize}
+Isabelle checks for 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.
 
 \index{examples!of theories} 
 This theory extends first-order logic by declaring and defining two constants,
@@ -438,6 +443,27 @@
 end
 \end{ttbox}
 
+Declaring and defining constants can be combined:
+\begin{ttbox}
+Gate = FOL +
+constdefs  nand :: [o,o] => o
+           "nand(P,Q) == ~(P & Q)"
+           xor  :: [o,o] => o
+           "xor(P,Q)  == P & ~Q | ~P & Q"
+end
+\end{ttbox}
+{\tt constdefs} generates the names {\tt nand_def} and {\tt xor_def}
+automatically, which is why it is restricted to alphanumeric identifiers. In
+general it has the form
+\begin{ttbox}
+constdefs  \(id@1\) :: \(\tau@1\)
+           "\(id@1 \equiv \dots\)"
+           \vdots
+           \(id@n\) :: \(\tau@n\)
+           "\(id@n \equiv \dots\)"
+\end{ttbox}
+
+
 \begin{warn}
 A common mistake when writing definitions is to introduce extra free variables
 on the right-hand side as in the following fictitious definition: