equal
deleted
inserted
replaced
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/} \\[2ex] |
9 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex] |
10 With Contributions by Gertrud Bauer and Tobias Nipkow} |
10 With contributions by Gertrud Bauer and Tobias Nipkow} |
11 \maketitle |
11 \maketitle |
12 |
12 |
13 \begin{abstract} |
13 \begin{abstract} |
14 Isar offers a high-level proof (and theory) language for Isabelle. |
14 Isar offers a high-level proof (and theory) language for Isabelle. |
15 We give various examples of Isabelle/Isar proof developments, |
15 We give various examples of Isabelle/Isar proof developments, |