# HG changeset patch
# User nipkow
# Date 790541209 -3600
# Node ID e1a654c29b05c87465679a92d61fe00ce46697bd
# Parent  2d3d020eef1168446c17d56a1114a6424ecc935b
some cosmetic changes

diff -r 2d3d020eef11 -r e1a654c29b05 doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Thu Jan 19 16:05:21 1995 +0100
+++ b/doc-src/Ref/defining.tex	Thu Jan 19 19:46:49 1995 +0100
@@ -188,12 +188,19 @@
   \verb!x<(y::nat)!.
 \end{warn}
 
-Isabelle's representation of mathematical languages is based on the simply
-typed $\lambda$-calculus\index{lambda calc@$\lambda$-calculus}.  All user
-defined logical types, namely those of class \cldx{logic}, refer to the
-nonterminal {\tt logic}. Thus they are automatically equipped with a basic
-syntax of types, identifiers, variables, parentheses, $\lambda$-abstractions
-and applications.
+\subsection{Logical types and default syntax}\label{logical-types}
+\index{lambda calc@$\lambda$-calculus}
+
+Isabelle's representation of mathematical languages is based on the
+simply typed $\lambda$-calculus.  All logical types, namely those of
+class \cldx{logic}, are automatically equipped with a basic syntax of
+types, identifiers, variables, parentheses, $\lambda$-abstraction and
+application.
+\begin{warn}
+  Isabelle combines the syntaxes for all types of class \cldx{logic} by
+  mapping all those types to the single nonterminal $logic$.  Thus all
+  productions of $logic$, in particular $id$, $var$ etc, become available.
+\end{warn}
 
 
 \subsection{Lexical matters}
@@ -488,11 +495,6 @@
 is sensible only if~$c$ is an identifier.  Otherwise you will be unable to
 write terms involving~$c$.
 
-\medskip 
-There is something artificial about the representation of productions as
-mixfix declarations, but it is convenient, particularly for simple theory
-extensions.
-
 
 \subsection{Example: arithmetic expressions}
 \index{examples!of mixfix declarations}
@@ -539,6 +541,12 @@
 {\out exp = "-" exp[3]  => "-" (3)}
 \end{ttbox}
 
+Note that because {\tt exp} is not of class {\tt logic}, it has been retained
+as a separate nonterminal. This also entails that the syntax does not provide
+for identifiers or paranthesized expressions. Normally you would also want to
+add the declaration {\tt arities exp :: logic} and use {\tt consts} instead
+of {\tt syntax}. Try this as an exercise and study the changes in the
+grammar.
 
 \subsection{The mixfix template}
 Let us now take a closer look at the string $template$ appearing in mixfix