doc-src/HOL/logics-HOL.tex
 changeset 13028 81c87faed78b parent 9695 ec7d7f877712 child 17659 b1019337c857
equal inserted replaced
13027:ddf235f2384a 13028:81c87faed78b
    42 \maketitle
    42 \maketitle
    43
    43
    44 \begin{abstract}
    44 \begin{abstract}
    45   This manual describes Isabelle's formalization of Higher-Order Logic, a
    45   This manual describes Isabelle's formalization of Higher-Order Logic, a
    46   polymorphic version of Church's Simple Theory of Types.  HOL can be best
    46   polymorphic version of Church's Simple Theory of Types.  HOL can be best
    47   understood as a simply-typed version of classical set theory.  See also
    47   understood as a simply-typed version of classical set theory.  The monograph
    48   \emph{Isabelle/HOL --- The Tutorial} for a gentle introduction on using
    48   \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
    49   Isabelle/HOL, and the \emph{Isabelle Reference Manual} for general Isabelle
    49   gentle introduction on using Isabelle/HOL in practice.
    50   commands.

    51 \end{abstract}
    50 \end{abstract}
    52
    51
    53 \pagenumbering{roman} \tableofcontents \clearfirst
    52 \pagenumbering{roman} \tableofcontents \clearfirst
    54 \input{../Logics/syntax}
    53 \input{../Logics/syntax}
    55 \include{HOL}
    54 \include{HOL}