--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Overview/IsaMakefile Mon Jul 01 15:41:07 2002 +0200
@@ -0,0 +1,25 @@
+## targets
+
+default: LNCS
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+USEDIR = $(ISATOOL) usedir -i true -d ps -D document -v true
+
+
+## LNCS
+
+LNCS: $(LOG)/HOL-LNCS.gz
+
+$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/*.thy
+ @$(USEDIR) HOL LNCS
+
+
+## clean
+
+clean:
+ @rm -f $(LOG)/HOL-LNCS.gz
+
--- 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}