diff -r 165f733c50bd -r c82dd66560ac doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Tue May 08 15:01:33 2007 +0200
+++ b/doc-src/IsarImplementation/implementation.tex	Tue May 08 15:36:39 2007 +0200
@@ -66,7 +66,7 @@
 \listoffigures
 \clearfirst
 
-\input{intro.tex}
+%\input{intro.tex}
 \input{Thy/document/prelim.tex}
 \input{Thy/document/logic.tex}
 \input{Thy/document/tactic.tex}