# HG changeset patch
# User paulson
# Date 839859962 -7200
# Node ID 81061bd61ad347d5584d967edeeb154e121b740d
# Parent  4f77c2fd8f3dd95b4413f320b1c8a8e4d779b64c
Added a new section on Definitions

diff -r 4f77c2fd8f3d -r 81061bd61ad3 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon Aug 12 16:25:08 1996 +0200
+++ b/doc-src/Ref/theories.tex	Mon Aug 12 16:26:02 1996 +0200
@@ -117,9 +117,8 @@
   given by the $string$.  Rule names must be distinct within any single
   theory file.
 
-\item[$defs$]
-  is a series of definitions.  Just like $rules$, except that every $string$
-  must be a definition.
+\item[$defs$] is a series of definitions.  They are just like $rules$, except
+  that every $string$ must be a definition (see below for details).
 
 \item[$constdefs$] combines the declaration of constants and their
   definition. The first $string$ is the type, the second the definition.
@@ -136,6 +135,29 @@
 declarations, translation rules and the {\tt ML} section in more detail.
 
 
+\subsection{Definitions}\indexbold{definitions}
+
+{\bf Definitions} are intended to express abbreviations. The simplest form of
+a definition is $f \equiv t$, where $f$ is a constant. Isabelle also allows a
+derived form where the arguments of~$f$ appear on the left, abbreviating a
+string of $\lambda$-abstractions.
+
+Isabelle makes the following checks on definitions:
+\begin{itemize}
+\item Arguments (on the left-hand side) must be distinct variables
+\item All variables on the right-hand side must also appear on the left-hand
+  side. 
+\item All type variables on the right-hand side must also appear on the
+  left-hand side; this prohibits definitions such as {\tt zero == length []}.
+\item The definition must not be recursive.  Most object-logics provide
+  definitional principles that can be used to express recursion safely.
+\end{itemize}
+These checks are intended to catch the sort of errors that might be made
+accidentally.  Misspellings, for instance, might result in additional
+variables appearing on the right-hand side.  More elaborate checks could be
+made, but the cost might be overly strict rules on declaration order, etc.
+
+
 \subsection{*Classes and arities}
 \index{classes!context conditions}\index{arities!context conditions}