# HG changeset patch
# User wenzelm
# Date 1272311108 -7200
# Node ID 5ab0f8859f9f32f6939e140e831f7cecb64f0d72
# Parent  aaa9933039b3a7674f17ec39e866cdc29caf71c3
command 'example_proof' opens an empty proof body;

diff -r aaa9933039b3 -r 5ab0f8859f9f NEWS
--- a/NEWS	Mon Apr 26 21:36:44 2010 +0200
+++ b/NEWS	Mon Apr 26 21:45:08 2010 +0200
@@ -103,6 +103,9 @@
 datatype constructors have been renamed from InfixName to Infix etc.
 Minor INCOMPATIBILITY.
 
+* Command 'example_proof' opens an empty proof body.  This allows to
+experiment with Isar, without producing any persistent result.
+
 * Commands 'type_notation' and 'no_type_notation' declare type syntax
 within a local theory context, with explicit checking of the
 constructors involved (in contrast to the raw 'syntax' versions).
diff -r aaa9933039b3 -r 5ab0f8859f9f doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 26 21:36:44 2010 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 26 21:45:08 2010 +0200
@@ -46,6 +46,28 @@
 
 section {* Proof structure *}
 
+subsection {* Example proofs *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item @{command "example_proof"} opens an empty proof body.  This
+  allows to experiment with Isar, without producing any persistent
+  result.
+
+  Structurally, this is like a vacous @{command "lemma"} statement
+  followed by ``@{command "proof"}~@{text "-"}'', which means the
+  example proof may be closed by a regular @{command "qed"}, or
+  discontinued by @{command "oops"}.
+
+  \end{description}
+*}
+
+
 subsection {* Blocks *}
 
 text {*
diff -r aaa9933039b3 -r 5ab0f8859f9f doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 26 21:36:44 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 26 21:45:08 2010 +0200
@@ -65,6 +65,30 @@
 }
 \isamarkuptrue%
 %
+\isamarkupsubsection{Example proofs%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \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}} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body.  This
+  allows to experiment with Isar, without producing any persistent
+  result.
+
+  Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
+  followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the
+  example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
+  discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Blocks%
 }
 \isamarkuptrue%
diff -r aaa9933039b3 -r 5ab0f8859f9f etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Apr 26 21:36:44 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Apr 26 21:45:08 2010 +0200
@@ -66,6 +66,7 @@
     "done"
     "enable_pr"
     "end"
+    "example_proof"
     "exit"
     "extract"
     "extract_type"
@@ -425,6 +426,7 @@
 
 (defconst isar-keywords-theory-goal
   '("corollary"
+    "example_proof"
     "instance"
     "interpretation"
     "lemma"
diff -r aaa9933039b3 -r 5ab0f8859f9f etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Apr 26 21:36:44 2010 +0200
+++ b/etc/isar-keywords.el	Mon Apr 26 21:45:08 2010 +0200
@@ -94,6 +94,7 @@
     "enable_pr"
     "end"
     "equivariance"
+    "example_proof"
     "exit"
     "export_code"
     "extract"
@@ -562,6 +563,7 @@
     "code_pred"
     "corollary"
     "cpodef"
+    "example_proof"
     "function"
     "instance"
     "interpretation"
diff -r aaa9933039b3 -r 5ab0f8859f9f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Apr 26 21:36:44 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 26 21:45:08 2010 +0200
@@ -510,6 +510,13 @@
 val _ = gen_theorem true Thm.corollaryK;
 
 val _ =
+  OuterSyntax.local_theory_to_proof "example_proof"
+    "example proof body, without any result" K.thy_schematic_goal
+    (Scan.succeed
+      (Specification.schematic_theorem_cmd "" NONE (K I)
+        Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
+
+val _ =
   OuterSyntax.command "have" "state local goal"
     (K.tag_proof K.prf_goal)
     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));