--- a/doc-src/HOL/HOL.tex Wed Mar 06 14:48:21 2002 +0100
+++ b/doc-src/HOL/HOL.tex Wed Mar 06 16:18:45 2002 +0100
@@ -2782,11 +2782,13 @@
constscode : 'consts_code' (codespec +);
-codespec : name ( () | '::' type) '(' mixfix ')';
+codespec : name ( () | '::' type) template;
typescode : 'types_code' (tycodespec +);
-tycodespec : name '(' mixfix ')';
+tycodespec : name template;
+
+template: '(' string ')';
\end{rail}
\caption{Code generator syntax}
\label{fig:HOL:codegen}
--- a/doc-src/HOL/logics-HOL.tex Wed Mar 06 14:48:21 2002 +0100
+++ b/doc-src/HOL/logics-HOL.tex Wed Mar 06 16:18:45 2002 +0100
@@ -44,10 +44,9 @@
\begin{abstract}
This manual describes Isabelle's formalization of Higher-Order Logic, a
polymorphic version of Church's Simple Theory of Types. HOL can be best
- understood as a simply-typed version of classical set theory. See also
- \emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
- Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
- commands.
+ understood as a simply-typed version of classical set theory. The monograph
+ \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
+ gentle introduction on using Isabelle/HOL in practice.
\end{abstract}
\pagenumbering{roman} \tableofcontents \clearfirst