diff -r 33d95687514e -r 854c61598628 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Mon Jun 02 21:19:46 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Jun 02 22:50:19 2008 +0200
@@ -19,12 +19,13 @@
   With Contributions by
   Clemens Ballarin,
   Stefan Berghofer, \\
+  Lucas Dixon,
   Florian Haftmann,
-  Gerwin Klein,
-  Alexander Krauss, \\
+  Gerwin Klein, \\
+  Alexander Krauss,
   Tobias Nipkow,
-  David von Oheimb,
-  Larry Paulson, \\
+  David von Oheimb, \\
+  Larry Paulson,
   and Sebastian Skalberg
 }
 
@@ -74,11 +75,11 @@
 \pagenumbering{roman} \tableofcontents \clearfirst
 
 \input{Thy/document/Introduction.tex}
-\input{basics.tex}
 \input{Thy/document/Outer_Syntax.tex}
 \input{Thy/document/Spec.tex}
 \input{Thy/document/Proof.tex}
 \input{Thy/document/pure.tex}
+\input{Thy/document/Document_Preparation.tex}
 \input{Thy/document/Generic.tex}
 \input{Thy/document/HOL_Specific.tex}
 \input{Thy/document/HOLCF_Specific.tex}