equal
deleted
inserted
replaced
11 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex] |
11 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex] |
12 With contributions by Gertrud Bauer and Tobias Nipkow} |
12 With contributions by Gertrud Bauer and Tobias Nipkow} |
13 \maketitle |
13 \maketitle |
14 |
14 |
15 \begin{abstract} |
15 \begin{abstract} |
16 Isar offers a high-level proof (and theory) language for Isabelle. We give |
16 Isar offers a high-level proof (and theory) language for Isabelle. |
17 various examples of Isabelle/Isar proof developments, ranging from simple |
17 We give various examples of Isabelle/Isar proof developments, |
18 demonstrations of certain language features to a bit more advanced |
18 ranging from simple demonstrations of certain language features to a |
19 applications. Note that the ``real'' applications of Isar are found |
19 bit more advanced applications. The ``real'' applications of |
20 elsewhere. |
20 Isabelle/Isar are found elsewhere. |
21 \end{abstract} |
21 \end{abstract} |
22 |
22 |
23 \tableofcontents |
23 \tableofcontents |
24 |
24 |
25 \parindent 0pt \parskip 0.5ex |
25 \parindent 0pt \parskip 0.5ex |