--- 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%
%