1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 26 21:36:44 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 26 21:45:08 2010 +0200
     1.3 @@ -65,6 +65,30 @@
     1.4  }
     1.5  \isamarkuptrue%
     1.6  %
     1.7 +\isamarkupsubsection{Example proofs%
     1.8 +}
     1.9 +\isamarkuptrue%
    1.10 +%
    1.11 +\begin{isamarkuptext}%
    1.12 +\begin{matharray}{rcl}
    1.13 +    \indexdef{}{command}{example\_proof}\hypertarget{command.example-proof}{\hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\
    1.14 +  \end{matharray}
    1.15 +
    1.16 +  \begin{description}
    1.17 +
    1.18 +  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body.  This
    1.19 +  allows to experiment with Isar, without producing any persistent
    1.20 +  result.
    1.21 +
    1.22 +  Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
    1.23 +  followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the
    1.24 +  example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
    1.25 +  discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    1.26 +
    1.27 +  \end{description}%
    1.28 +\end{isamarkuptext}%
    1.29 +\isamarkuptrue%
    1.30 +%
    1.31  \isamarkupsubsection{Blocks%
    1.32  }
    1.33  \isamarkuptrue%