--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Sat May 10 20:53:02 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-\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}