tuned;
authorwenzelm
Wed Mar 06 16:18:45 2002 +0100 (2002-03-06)
changeset 1302881c87faed78b
parent 13027 ddf235f2384a
child 13029 84e4ba7fb033
tuned;
doc-src/HOL/HOL.tex
doc-src/HOL/logics-HOL.tex
     1.1 --- a/doc-src/HOL/HOL.tex	Wed Mar 06 14:48:21 2002 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Wed Mar 06 16:18:45 2002 +0100
     1.3 @@ -2782,11 +2782,13 @@
     1.4  
     1.5  constscode : 'consts_code' (codespec +);
     1.6  
     1.7 -codespec : name ( () | '::' type) '(' mixfix ')';
     1.8 +codespec : name ( () | '::' type) template;
     1.9  
    1.10  typescode : 'types_code' (tycodespec +);
    1.11  
    1.12 -tycodespec : name '(' mixfix ')';
    1.13 +tycodespec : name template;
    1.14 +
    1.15 +template: '(' string ')';
    1.16  \end{rail}
    1.17  \caption{Code generator syntax}
    1.18  \label{fig:HOL:codegen}
     2.1 --- a/doc-src/HOL/logics-HOL.tex	Wed Mar 06 14:48:21 2002 +0100
     2.2 +++ b/doc-src/HOL/logics-HOL.tex	Wed Mar 06 16:18:45 2002 +0100
     2.3 @@ -44,10 +44,9 @@
     2.4  \begin{abstract}
     2.5    This manual describes Isabelle's formalization of Higher-Order Logic, a
     2.6    polymorphic version of Church's Simple Theory of Types.  HOL can be best
     2.7 -  understood as a simply-typed version of classical set theory.  See also
     2.8 -  \emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
     2.9 -  Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
    2.10 -  commands.
    2.11 +  understood as a simply-typed version of classical set theory.  The monograph
    2.12 +  \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
    2.13 +  gentle introduction on using Isabelle/HOL in practice.
    2.14  \end{abstract}
    2.15  
    2.16  \pagenumbering{roman} \tableofcontents \clearfirst