7741
|
1 |
|
|
2 |
\input{style}
|
|
3 |
|
|
4 |
\hyphenation{Isabelle}
|
|
5 |
|
|
6 |
\begin{document}
|
|
7 |
|
|
8 |
\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
|
|
9 |
\author{Markus Wenzel}
|
|
10 |
\maketitle
|
|
11 |
|
|
12 |
\begin{abstract}
|
|
13 |
Isar offers a high-level proof (and theory) language interface to Isabelle.
|
|
14 |
We give various examples of Isabelle/Isar proof developments, ranging from
|
|
15 |
simple demonstrations of certain language features to more advanced
|
|
16 |
applications.
|
|
17 |
\end{abstract}
|
|
18 |
|
|
19 |
\tableofcontents
|
|
20 |
\input{session}
|
|
21 |
|
|
22 |
\end{document}
|