equal
deleted
inserted
replaced
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} |