1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 26 21:36:44 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 26 21:45:08 2010 +0200
     1.3 @@ -46,6 +46,28 @@
     1.4  
     1.5  section {* Proof structure *}
     1.6  
     1.7 +subsection {* Example proofs *}
     1.8 +
     1.9 +text {*
    1.10 +  \begin{matharray}{rcl}
    1.11 +    @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
    1.12 +  \end{matharray}
    1.13 +
    1.14 +  \begin{description}
    1.15 +
    1.16 +  \item @{command "example_proof"} opens an empty proof body.  This
    1.17 +  allows to experiment with Isar, without producing any persistent
    1.18 +  result.
    1.19 +
    1.20 +  Structurally, this is like a vacous @{command "lemma"} statement
    1.21 +  followed by ``@{command "proof"}~@{text "-"}'', which means the
    1.22 +  example proof may be closed by a regular @{command "qed"}, or
    1.23 +  discontinued by @{command "oops"}.
    1.24 +
    1.25 +  \end{description}
    1.26 +*}
    1.27 +
    1.28 +
    1.29  subsection {* Blocks *}
    1.30  
    1.31  text {*