some cosmetic changes
Thu, 19 Jan 1995 19:46:49 +0100
changeset 867 e1a654c29b05
parent 866 2d3d020eef11
child 868 452f1e6ae3bc
some cosmetic changes
--- 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 @@
-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
+  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.
 \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$.
-There is something artificial about the representation of productions as
-mixfix declarations, but it is convenient, particularly for simple theory
 \subsection{Example: arithmetic expressions}
 \index{examples!of mixfix declarations}
@@ -539,6 +541,12 @@
 {\out exp = "-" exp[3]  => "-" (3)}
+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
 \subsection{The mixfix template}
 Let us now take a closer look at the string $template$ appearing in mixfix