diff -r 5072d6c77baa -r cd8d99b9ef09 doc-src/IsarRef/Thy/Introduction.thy
--- a/doc-src/IsarRef/Thy/Introduction.thy	Mon Jun 02 23:38:24 2008 +0200
+++ b/doc-src/IsarRef/Thy/Introduction.thy	Mon Jun 02 23:38:25 2008 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory Introduction
-imports Pure
+imports Main
 begin
 
 chapter {* Introduction *}
@@ -73,7 +73,7 @@
 *}
 
 
-section {* Quick start *}
+section {* User interfaces *}
 
 subsection {* Terminal sessions *}
 
@@ -227,7 +227,7 @@
 *}
 
 
-subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
+section {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
 
 text {*
   This is one of the key questions, of course.  First of all, the