--- 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
--- 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}
*}
--- 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}%
--- 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"
--- 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"
--- 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));