diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 22:55:49 2006 +0200
@@ -3,11 +3,9 @@
 
 theory "proof" imports base begin
 
-chapter {* Structured reasoning *}
+chapter {* Structured proofs *}
 
-section {* Proof context *}
-
-subsection {* Local variables *}
+section {* Local variables *}
 
 text FIXME
 
@@ -66,7 +64,23 @@
 
 text FIXME
 
-section {* Proof state *}
+
+section {* Schematic polymorphism *}
+
+text FIXME
+
+
+section {* Assumptions *}
+
+text FIXME
+
+
+section {* Conclusions *}
+
+text FIXME
+
+
+section {* Structured proofs \label{sec:isar-proof-state} *}
 
 text {*
   FIXME
@@ -85,12 +99,12 @@
 
 *}
 
-section {* Methods *}
+section {* Proof methods *}
 
 text FIXME
 
 section {* Attributes *}
 
-text FIXME
+text "FIXME ?!"
 
 end