diff -r ff7d6a847929 -r b07c46e67e2d doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Sat May 13 02:51:33 2006 +0200
+++ b/doc-src/Ref/theories.tex	Sat May 13 02:51:35 2006 +0200
@@ -181,30 +181,6 @@
 declarations, translation rules and the \texttt{ML} section in more detail.
 
 
-\subsection{Definitions}\indexbold{definitions}
-
-\textbf{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 forms 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::nat) == length ([]::'a list)}.
-\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}