Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)
\input{style}
\hyphenation{Isabelle}
\begin{document}
\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex]
With contributions by Gertrud Bauer and Tobias Nipkow}
\maketitle
\begin{abstract}
Isar offers a high-level proof (and theory) language for Isabelle.
We give various examples of Isabelle/Isar proof developments,
ranging from simple demonstrations of certain language features to a
bit more advanced applications. The ``real'' applications of
Isabelle/Isar are found elsewhere.
\end{abstract}
\tableofcontents
\parindent 0pt \parskip 0.5ex
\input{session}
\nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}