1.1 --- a/NEWS	Mon Apr 26 21:36:44 2010 +0200
     1.2 +++ b/NEWS	Mon Apr 26 21:45:08 2010 +0200
     1.3 @@ -103,6 +103,9 @@
     1.4  datatype constructors have been renamed from InfixName to Infix etc.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Command 'example_proof' opens an empty proof body.  This allows to
     1.8 +experiment with Isar, without producing any persistent result.
     1.9 +
    1.10  * Commands 'type_notation' and 'no_type_notation' declare type syntax
    1.11  within a local theory context, with explicit checking of the
    1.12  constructors involved (in contrast to the raw 'syntax' versions).

     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 26 21:36:44 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 26 21:45:08 2010 +0200
     2.3 @@ -46,6 +46,28 @@
     2.4  
     2.5  section {* Proof structure *}
     2.6  
     2.7 +subsection {* Example proofs *}
     2.8 +
     2.9 +text {*
    2.10 +  \begin{matharray}{rcl}
    2.11 +    @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
    2.12 +  \end{matharray}
    2.13 +
    2.14 +  \begin{description}
    2.15 +
    2.16 +  \item @{command "example_proof"} opens an empty proof body.  This
    2.17 +  allows to experiment with Isar, without producing any persistent
    2.18 +  result.
    2.19 +
    2.20 +  Structurally, this is like a vacous @{command "lemma"} statement
    2.21 +  followed by ``@{command "proof"}~@{text "-"}'', which means the
    2.22 +  example proof may be closed by a regular @{command "qed"}, or
    2.23 +  discontinued by @{command "oops"}.
    2.24 +
    2.25 +  \end{description}
    2.26 +*}
    2.27 +
    2.28 +
    2.29  subsection {* Blocks *}
    2.30  
    2.31  text {*

     3.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 26 21:36:44 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 26 21:45:08 2010 +0200
     3.3 @@ -65,6 +65,30 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 +\isamarkupsubsection{Example proofs%
     3.8 +}
     3.9 +\isamarkuptrue%
    3.10 +%
    3.11 +\begin{isamarkuptext}%
    3.12 +\begin{matharray}{rcl}
    3.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}} \\
    3.14 +  \end{matharray}
    3.15 +
    3.16 +  \begin{description}
    3.17 +
    3.18 +  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body.  This
    3.19 +  allows to experiment with Isar, without producing any persistent
    3.20 +  result.
    3.21 +
    3.22 +  Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
    3.23 +  followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the
    3.24 +  example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
    3.25 +  discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    3.26 +
    3.27 +  \end{description}%
    3.28 +\end{isamarkuptext}%
    3.29 +\isamarkuptrue%
    3.30 +%
    3.31  \isamarkupsubsection{Blocks%
    3.32  }
    3.33  \isamarkuptrue%

     4.1 --- a/etc/isar-keywords-ZF.el	Mon Apr 26 21:36:44 2010 +0200
     4.2 +++ b/etc/isar-keywords-ZF.el	Mon Apr 26 21:45:08 2010 +0200
     4.3 @@ -66,6 +66,7 @@
     4.4      "done"
     4.5      "enable_pr"
     4.6      "end"
     4.7 +    "example_proof"
     4.8      "exit"
     4.9      "extract"
    4.10      "extract_type"
    4.11 @@ -425,6 +426,7 @@
    4.12  
    4.13  (defconst isar-keywords-theory-goal
    4.14    '("corollary"
    4.15 +    "example_proof"
    4.16      "instance"
    4.17      "interpretation"
    4.18      "lemma"

     5.1 --- a/etc/isar-keywords.el	Mon Apr 26 21:36:44 2010 +0200
     5.2 +++ b/etc/isar-keywords.el	Mon Apr 26 21:45:08 2010 +0200
     5.3 @@ -94,6 +94,7 @@
     5.4      "enable_pr"
     5.5      "end"
     5.6      "equivariance"
     5.7 +    "example_proof"
     5.8      "exit"
     5.9      "export_code"
    5.10      "extract"
    5.11 @@ -562,6 +563,7 @@
    5.12      "code_pred"
    5.13      "corollary"
    5.14      "cpodef"
    5.15 +    "example_proof"
    5.16      "function"
    5.17      "instance"
    5.18      "interpretation"

     6.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Apr 26 21:36:44 2010 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 26 21:45:08 2010 +0200
     6.3 @@ -510,6 +510,13 @@
     6.4  val _ = gen_theorem true Thm.corollaryK;
     6.5  
     6.6  val _ =
     6.7 +  OuterSyntax.local_theory_to_proof "example_proof"
     6.8 +    "example proof body, without any result" K.thy_schematic_goal
     6.9 +    (Scan.succeed
    6.10 +      (Specification.schematic_theorem_cmd "" NONE (K I)
    6.11 +        Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
    6.12 +
    6.13 +val _ =
    6.14    OuterSyntax.command "have" "state local goal"
    6.15      (K.tag_proof K.prf_goal)
    6.16      (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));