diff -r 88ff12baccba -r 0090fab725e3 doc-src/TutorialI/Overview/LNCS/document/root.tex
--- a/doc-src/TutorialI/Overview/LNCS/document/root.tex	Mon Jul 30 16:40:21 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +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\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\
- \small\url{http://www.in.tum.de/~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}
-
-\begin{exercise}
-Define a datatype of binary trees and a function \isa{mirror}
-that mirrors a binary tree by swapping subtrees recursively. Prove
-\isa{mirror(mirror t) = t}.
-
-Define a function \isa{flatten} that flattens a tree into a list
-by traversing it in infix order. Prove
-\isa{flatten(mirror t) = rev(flatten t)}.
-\end{exercise}
-
-\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}