--- a/doc-src/TutorialI/Overview/document/root.tex Mon Jul 01 15:33:03 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym,pdfsetup}
-
-%for best-style documents ...
-\urlstyle{rm}
-%\isabellestyle{it}
-
-\newtheorem{Exercise}{Exercise}[section]
-\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
-
-\begin{document}
-
-\title{A Compact Overview of Isabelle/HOL}
-\author{Tobias Nipkow}
-\date{}
-\maketitle
-
-\noindent
-This document is a very compact introduction to the proof assistant
-Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283}
-where full explanations and a wealth of additional material can be found.
-
-While reading this document it is recommended to single-step through the
-corresponding theories using Isabelle/HOL to follow the proofs.
-
-\section{Functional Programming/Modelling}
-
-\subsection{An Introductory Theory}
-\input{FP0.tex}
-
-\subsection{More Constructs}
-\input{FP1.tex}
-
-\input{RECDEF.tex}
-
-\input{Rules.tex}
-
-\input{Sets.tex}
-
-\input{Ind.tex}
-
-%\input{Isar.tex}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
-
-
-\bibliographystyle{plain}
-\bibliography{root}
-
-\end{document}