doc-src/IsarOverview/Isar/document/root.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarOverview/Isar/document/root.tex	Mon May 12 11:33:55 2003 +0200
@@ -0,0 +1,50 @@
+\documentclass[envcountsame]{llncs}
+%\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+%for best-style documents ...
+\urlstyle{rm}
+%\isabellestyle{it}
+
+\newcommand{\tweakskip}{\vspace{-\medskipamount}}
+\newcommand{\Tweakskip}{\tweakskip\tweakskip}
+
+\pagestyle{plain}
+
+\begin{document}
+
+\title{%A Compact Introduction to
+Structured Proofs in Isar/HOL}
+\author{Tobias Nipkow}
+\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
+ {\small\url{http://www.in.tum.de/~nipkow/}}}
+\date{}
+\maketitle
+
+\begin{abstract}
+  Isar is an extension of the theorem prover Isabelle with a language
+  for writing human-readable structured proofs. This paper is an
+  introduction to the basic constructs of this language.
+% It is aimed at potential users of Isar
+% but also discusses the design rationals
+% behind the language and its constructs.
+\end{abstract}
+
+\input{intro.tex}
+\input{Logic.tex}
+\Tweakskip\Tweakskip
+\input{Induction.tex}
+
+%\Tweakskip
+\small
+\paragraph{Acknowledgement}
+I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
+Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer,
+Markus Wenzel and Freek Wiedijk commented on and improved this paper.
+
+\begingroup
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{root}
+\endgroup
+
+\end{document}