diff -r a53dfe909674 -r 5c48cecb981b doc-src/IsarRef/Thy/document/Introduction.tex
--- a/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Jun 02 23:38:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Jun 02 23:38:28 2008 +0200
@@ -11,7 +11,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Introduction\isanewline
-\isakeyword{imports}\ Pure\isanewline
+\isakeyword{imports}\ Main\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
@@ -92,7 +92,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Quick start%
+\isamarkupsection{User interfaces%
 }
 \isamarkuptrue%
 %
@@ -255,7 +255,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
+\isamarkupsection{How to write Isar proofs anyway? \label{sec:isar-howto}%
 }
 \isamarkuptrue%
 %