# HG changeset patch
# User wenzelm
# Date 1212442705 -7200
# Node ID cd8d99b9ef099c49dcde92eeee3f57e25d975f27
# Parent  5072d6c77baa88aac00525401b8afa6d71071f14
tuned structure;

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
diff -r 5072d6c77baa -r cd8d99b9ef09 doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Mon Jun 02 23:38:24 2008 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Mon Jun 02 23:38:25 2008 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory Outer_Syntax
-imports Pure
+imports Main
 begin
 
 chapter {* Outer syntax *}