doc-src/IsarRef/Thy/Introduction.thy
changeset 27050 cd8d99b9ef09
parent 27040 3d3e6e07b931
child 27058 3dcd890b0bf2
--- 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