Lines Matching refs:to
4 %% run bibtex intro to prepare bibliography
5 %% run ../sedindex intro to prepare index file
9 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}
36 syntax and shows how to conduct proofs using the
52 prover. It has been instantiated to support reasoning in several
56 \item higher-order logic, similar to that of Gordon's {\sc
68 which can be applied to object-logics.
72 The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
75 if you are prepared to writing \ML{}
76 code, you can get Isabelle to do almost anything. My book
85 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an
95 pretty printer generator. The 1992 version introduced type classes, to
98 introduction of the Isar proof language, thanks to Markus Wenzel.
100 development and will continue to change.
107 with a bit of experience. It explains how to derive rules define theories,
118 Tobias Nipkow has made immense contributions to Isabelle, including the parser
122 compiler, Poly/{\sc ml}. Many people have contributed to Isabelle's standard