equal
deleted
inserted
replaced
4 \hyphenation{Isabelle} |
4 \hyphenation{Isabelle} |
5 |
5 |
6 \begin{document} |
6 \begin{document} |
7 |
7 |
8 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic} |
8 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic} |
9 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/}} |
9 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex] |
|
10 With Contributions by Gertrud Bauer and Tobias Nipkow} |
10 \maketitle |
11 \maketitle |
11 |
12 |
12 \begin{abstract} |
13 \begin{abstract} |
13 Isar offers a high-level proof (and theory) language for Isabelle. |
14 Isar offers a high-level proof (and theory) language for Isabelle. |
14 We give various examples of Isabelle/Isar proof developments, |
15 We give various examples of Isabelle/Isar proof developments, |