1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun Dec 05 13:42:58 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sun Dec 05 14:02:16 2010 +0100
     1.3 @@ -65,25 +65,30 @@
     1.4  }
     1.5  \isamarkuptrue%
     1.6  %
     1.7 -\isamarkupsubsection{Example proofs%
     1.8 +\isamarkupsubsection{Formal notepad%
     1.9  }
    1.10  \isamarkuptrue%
    1.11  %
    1.12  \begin{isamarkuptext}%
    1.13  \begin{matharray}{rcl}
    1.14 -    \indexdef{}{command}{example\_proof}\hypertarget{command.example-proof}{\hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
    1.15 +    \indexdef{}{command}{notepad}\hypertarget{command.notepad}{\hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
    1.16    \end{matharray}
    1.17  
    1.18 +  \begin{rail}
    1.19 +    'notepad' 'begin'
    1.20 +    ;
    1.21 +    'end'
    1.22 +    ;
    1.23 +  \end{rail}
    1.24 +
    1.25    \begin{description}
    1.26  
    1.27 -  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}}}} opens an empty proof body.  This
    1.28 -  allows to experiment with Isar, without producing any persistent
    1.29 -  result.
    1.30 +  \item \hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} opens a proof state
    1.31 +  without any goal statement.  This allows to experiment with Isar,
    1.32 +  without producing any persistent result.
    1.33  
    1.34 -  Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
    1.35 -  followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'', which means the
    1.36 -  example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
    1.37 -  discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    1.38 +  The notepad can be closed by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} or discontinued by
    1.39 +  \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    1.40  
    1.41    \end{description}%
    1.42  \end{isamarkuptext}%