# HG changeset patch
# User lcp
# Date 799495461 -7200
# Node ID 502a61cbf37b1c32353c4a55987d62e160403750
# Parent  53a0667e1cd228b27c313803174b76188bdc9a01
Covers defs and re-ordering of theory sections

diff -r 53a0667e1cd2 -r 502a61cbf37b doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Wed May 03 11:58:40 1995 +0200
+++ b/doc-src/Intro/advanced.tex	Wed May 03 12:04:21 1995 +0200
@@ -339,6 +339,7 @@
 arities      {\it arity declarations}
 consts       {\it constant declarations}
 translations {\it translation declarations}
+defs         {\it constant definitions}
 rules        {\it rule declarations}
 end
 ML           {\it ML code}
@@ -355,10 +356,11 @@
 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
   appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
 
-All the declaration parts can be omitted.  In the simplest case, $T$ is
-just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
-or more other theories, inheriting their types, constants, syntax, etc.
-The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
+All the declaration parts can be omitted or repeated and may appear in any
+order, except that the {\ML} section must be last.  In the simplest case, $T$
+is just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one or
+more other theories, inheriting their types, constants, syntax, etc.  The
+theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
 
 Each theory definition must reside in a separate file, whose name is the
 theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
@@ -387,11 +389,11 @@
 for more details.
 
 
-\subsection{Declaring constants and rules}
+\subsection{Declaring constants, definitions and rules}
 \indexbold{constants!declaring}\index{rules!declaring}
 
-Most theories simply declare constants and rules.  The {\bf constant
-declaration part} has the form
+Most theories simply declare constants, definitions and rules.  The {\bf
+  constant declaration part} has the form
 \begin{ttbox}
 consts  \(c@1\) :: "\(\tau@1\)"
         \vdots
@@ -415,21 +417,22 @@
 $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
 enclosed in quotation marks.
 
-\indexbold{definitions}
-{\bf Definitions} are rules of the form $t\equiv u$.  Normally definitions
-should be conservative, serving only as abbreviations.  As of this writing,
-Isabelle does not provide a separate declaration part for definitions; it
-is your responsibility to ensure that your definitions are conservative.
-However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all
-variables free in~$u$ are also free in~$t$.
+\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-hard 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 with two constants {\em nand} and
-{\em xor}, and declares rules to define them:
+
+\index{examples!of theories} 
+This theory extends first-order logic by declaring and defining two constants,
+{\em nand} and {\em xor}:
 \begin{ttbox}
 Gate = FOL +
 consts  nand,xor :: "[o,o] => o"
-rules   nand_def "nand(P,Q) == ~(P & Q)"
+defs    nand_def "nand(P,Q) == ~(P & Q)"
         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
 end
 \end{ttbox}
@@ -555,7 +558,7 @@
 Gate2 = FOL +
 consts  "~&"     :: "[o,o] => o"         (infixl 35)
         "#"      :: "[o,o] => o"         (infixl 30)
-rules   nand_def "P ~& Q == ~(P & Q)"    
+defs    nand_def "P ~& Q == ~(P & Q)"    
         xor_def  "P # Q  == P & ~Q | ~P & Q"
 end
 \end{ttbox}
@@ -614,7 +617,7 @@
 Binary type constructors, like products and sums, may also be declared as
 infixes.  The type declaration below introduces a type constructor~$*$ with
 infix notation $\alpha*\beta$, together with the mixfix notation
-${<}\_,\_{>}$ for pairs.  
+${<}\_,\_{>}$ for pairs.  We also see a rule declaration part.
 \index{examples!of theories}\index{mixfix declarations}
 \begin{ttbox}
 Prod = FOL +