# HG changeset patch
# User wenzelm
# Date 939140213 -7200
# Node ID 874abb8aa65b5cf23ca1e4132e77723c868d7b46
# Parent  2fbe5ce9845f107e86beb87cbc9e924021b64c97
added document;

diff -r 2fbe5ce9845f -r 874abb8aa65b src/HOL/Isar_examples/document/root.tex
--- /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}