--- a/src/HOL/Isar_examples/document/root.tex Fri Feb 04 21:36:13 2000 +0100
+++ b/src/HOL/Isar_examples/document/root.tex Fri Feb 04 21:37:23 2000 +0100
@@ -20,7 +20,20 @@
\tableofcontents
\parindent 0pt \parskip 0.5ex
-\input{session}
+
+\input{BasicLogic.tex}
+\input{Cantor.tex}
+\input{Peirce.tex}
+\input{ExprCompiler.tex}
+\input{Group.tex}
+\input{Summation.tex}
+\input{KnasterTarski.tex}
+\input{MutilatedCheckerboard.tex}
+\input{MultisetOrder.tex}
+\input{W_correct.tex}
+\input{Primes.tex}
+\input{Fibonacci.tex}
+\input{Puzzle.tex}
\nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
\bibliographystyle{plain}