--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/document/root.tex Tue Oct 05 18:16:53 1999 +0200
@@ -0,0 +1,24 @@
+
+\input{style}
+
+\hyphenation{Isabelle}
+
+
+\begin{document}
+
+\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
+\author{Markus Wenzel}
+\maketitle
+
+\begin{abstract}
+ Isar offers a high-level proof (and theory) language interface to Isabelle.
+ We give various examples of Isabelle/Isar proof developments, ranging from
+ simple demonstrations of certain language features to more advanced
+ applications.
+\end{abstract}
+
+\tableofcontents
+
+\input{session}
+
+\end{document}