# HG changeset patch
# User wenzelm
# Date 1291554136 -3600
# Node ID 54b6c9e1c157ea4285156e7c3e7579130ebf633d
# Parent  482a8334ee9ef86e3f55816aafa34b2dd8ec6553
command 'notepad' replaces former 'example_proof';

diff -r 482a8334ee9e -r 54b6c9e1c157 NEWS
--- a/NEWS	Sun Dec 05 13:42:58 2010 +0100
+++ b/NEWS	Sun Dec 05 14:02:16 2010 +0100
@@ -83,6 +83,9 @@
 
 *** Pure ***
 
+* Command 'notepad' replaces former 'example_proof' for
+experimentation in Isar without and result.  INCOMPATIBILITY.
+
 * Support for real valued preferences (with approximative PGIP type).
 
 * Interpretation command 'interpret' accepts a list of equations like
diff -r 482a8334ee9e -r 54b6c9e1c157 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Sun Dec 05 13:42:58 2010 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Sun Dec 05 14:02:16 2010 +0100
@@ -46,23 +46,28 @@
 
 section {* Proof structure *}
 
-subsection {* Example proofs *}
+subsection {* Formal notepad *}
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
+    @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
   \end{matharray}
 
+  \begin{rail}
+    'notepad' 'begin'
+    ;
+    'end'
+    ;
+  \end{rail}
+
   \begin{description}
 
-  \item @{command "example_proof"} opens an empty proof body.  This
-  allows to experiment with Isar, without producing any persistent
-  result.
+  \item @{command "notepad"}~@{keyword "begin"} opens a proof state
+  without any goal statement.  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"}.
+  The notepad can be closed by @{command "end"} or discontinued by
+  @{command "oops"}.
 
   \end{description}
 *}
diff -r 482a8334ee9e -r 54b6c9e1c157 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun Dec 05 13:42:58 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sun Dec 05 14:02:16 2010 +0100
@@ -65,25 +65,30 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsubsection{Example proofs%
+\isamarkupsubsection{Formal notepad%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \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}}} \\
+    \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}}} \\
   \end{matharray}
 
+  \begin{rail}
+    'notepad' 'begin'
+    ;
+    'end'
+    ;
+  \end{rail}
+
   \begin{description}
 
-  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}}}} opens an empty proof body.  This
-  allows to experiment with Isar, without producing any persistent
-  result.
+  \item \hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} opens a proof state
+  without any goal statement.  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{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\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}}}}.
+  The notepad can be closed by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} or discontinued by
+  \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
 
   \end{description}%
 \end{isamarkuptext}%
diff -r 482a8334ee9e -r 54b6c9e1c157 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Dec 05 13:42:58 2010 +0100
+++ b/etc/isar-keywords-ZF.el	Sun Dec 05 14:02:16 2010 +0100
@@ -61,7 +61,6 @@
     "done"
     "enable_pr"
     "end"
-    "example_proof"
     "exit"
     "extract"
     "extract_type"
@@ -415,7 +414,6 @@
 
 (defconst isar-keywords-theory-goal
   '("corollary"
-    "example_proof"
     "instance"
     "interpretation"
     "lemma"
diff -r 482a8334ee9e -r 54b6c9e1c157 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Dec 05 13:42:58 2010 +0100
+++ b/etc/isar-keywords.el	Sun Dec 05 14:02:16 2010 +0100
@@ -86,7 +86,6 @@
     "enable_pr"
     "end"
     "equivariance"
-    "example_proof"
     "exit"
     "export_code"
     "extract"
@@ -533,7 +532,6 @@
     "code_pred"
     "corollary"
     "cpodef"
-    "example_proof"
     "function"
     "instance"
     "interpretation"
diff -r 482a8334ee9e -r 54b6c9e1c157 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Dec 05 13:42:58 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Dec 05 14:02:16 2010 +0100
@@ -513,13 +513,6 @@
     (Parse.begin >> K Proof.begin_notepad);
 
 val _ =
-  Outer_Syntax.local_theory_to_proof "example_proof"
-    "example proof body, without any result" Keyword.thy_schematic_goal
-    (Scan.succeed
-      (Specification.theorem_cmd "" NONE (K I)
-        Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
-
-val _ =
   Outer_Syntax.command "have" "state local goal"
     (Keyword.tag_proof Keyword.prf_goal)
     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));