1.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 18:27:40 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Aug 31 22:55:49 2006 +0200
     1.3 @@ -3,11 +3,9 @@
     1.4  
     1.5  theory "proof" imports base begin
     1.6  
     1.7 -chapter {* Structured reasoning *}
     1.8 +chapter {* Structured proofs *}
     1.9  
    1.10 -section {* Proof context *}
    1.11 -
    1.12 -subsection {* Local variables *}
    1.13 +section {* Local variables *}
    1.14  
    1.15  text FIXME
    1.16  
    1.17 @@ -66,7 +64,23 @@
    1.18  
    1.19  text FIXME
    1.20  
    1.21 -section {* Proof state *}
    1.22 +
    1.23 +section {* Schematic polymorphism *}
    1.24 +
    1.25 +text FIXME
    1.26 +
    1.27 +
    1.28 +section {* Assumptions *}
    1.29 +
    1.30 +text FIXME
    1.31 +
    1.32 +
    1.33 +section {* Conclusions *}
    1.34 +
    1.35 +text FIXME
    1.36 +
    1.37 +
    1.38 +section {* Structured proofs \label{sec:isar-proof-state} *}
    1.39  
    1.40  text {*
    1.41    FIXME
    1.42 @@ -85,12 +99,12 @@
    1.43  
    1.44  *}
    1.45  
    1.46 -section {* Methods *}
    1.47 +section {* Proof methods *}
    1.48  
    1.49  text FIXME
    1.50  
    1.51  section {* Attributes *}
    1.52  
    1.53 -text FIXME
    1.54 +text "FIXME ?!"
    1.55  
    1.56  end