# HG changeset patch
# User wenzelm
# Date 1015427925 -3600
# Node ID 81c87faed78b9b7c59de99fdd2441c116d3608bf
# Parent  ddf235f2384a736e67b53355c7db4a0d4a74cebc
tuned;

diff -r ddf235f2384a -r 81c87faed78b doc-src/HOL/HOL.tex
--- 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}
diff -r ddf235f2384a -r 81c87faed78b doc-src/HOL/logics-HOL.tex
--- 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