summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/HOL/logics-HOL.tex

changeset 13028 | 81c87faed78b |

parent 9695 | ec7d7f877712 |

child 17659 | b1019337c857 |

--- 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