command 'notepad' replaces former 'example_proof';
authorwenzelm
Sun Dec 05 14:02:16 2010 +0100 (2010-12-05)
changeset 4096554b6c9e1c157
parent 40964 482a8334ee9e
child 40966 d5a198eb16b5
child 40968 a6fcd305f7dc
child 40977 9140c5950494
command 'notepad' replaces former 'example_proof';
NEWS
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/document/Proof.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Sun Dec 05 13:42:58 2010 +0100
     1.2 +++ b/NEWS	Sun Dec 05 14:02:16 2010 +0100
     1.3 @@ -83,6 +83,9 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Command 'notepad' replaces former 'example_proof' for
     1.8 +experimentation in Isar without and result.  INCOMPATIBILITY.
     1.9 +
    1.10  * Support for real valued preferences (with approximative PGIP type).
    1.11  
    1.12  * Interpretation command 'interpret' accepts a list of equations like
     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Sun Dec 05 13:42:58 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Sun Dec 05 14:02:16 2010 +0100
     2.3 @@ -46,23 +46,28 @@
     2.4  
     2.5  section {* Proof structure *}
     2.6  
     2.7 -subsection {* Example proofs *}
     2.8 +subsection {* Formal notepad *}
     2.9  
    2.10  text {*
    2.11    \begin{matharray}{rcl}
    2.12 -    @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
    2.13 +    @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
    2.14    \end{matharray}
    2.15  
    2.16 +  \begin{rail}
    2.17 +    'notepad' 'begin'
    2.18 +    ;
    2.19 +    'end'
    2.20 +    ;
    2.21 +  \end{rail}
    2.22 +
    2.23    \begin{description}
    2.24  
    2.25 -  \item @{command "example_proof"} opens an empty proof body.  This
    2.26 -  allows to experiment with Isar, without producing any persistent
    2.27 -  result.
    2.28 +  \item @{command "notepad"}~@{keyword "begin"} opens a proof state
    2.29 +  without any goal statement.  This allows to experiment with Isar,
    2.30 +  without producing any persistent result.
    2.31  
    2.32 -  Structurally, this is like a vacous @{command "lemma"} statement
    2.33 -  followed by ``@{command "proof"}~@{text "-"}'', which means the
    2.34 -  example proof may be closed by a regular @{command "qed"}, or
    2.35 -  discontinued by @{command "oops"}.
    2.36 +  The notepad can be closed by @{command "end"} or discontinued by
    2.37 +  @{command "oops"}.
    2.38  
    2.39    \end{description}
    2.40  *}
     3.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun Dec 05 13:42:58 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sun Dec 05 14:02:16 2010 +0100
     3.3 @@ -65,25 +65,30 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsubsection{Example proofs%
     3.8 +\isamarkupsubsection{Formal notepad%
     3.9  }
    3.10  \isamarkuptrue%
    3.11  %
    3.12  \begin{isamarkuptext}%
    3.13  \begin{matharray}{rcl}
    3.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}}} \\
    3.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}}} \\
    3.16    \end{matharray}
    3.17  
    3.18 +  \begin{rail}
    3.19 +    'notepad' 'begin'
    3.20 +    ;
    3.21 +    'end'
    3.22 +    ;
    3.23 +  \end{rail}
    3.24 +
    3.25    \begin{description}
    3.26  
    3.27 -  \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isaliteral{5F}{\isacharunderscore}}proof}}}} opens an empty proof body.  This
    3.28 -  allows to experiment with Isar, without producing any persistent
    3.29 -  result.
    3.30 +  \item \hyperlink{command.notepad}{\mbox{\isa{\isacommand{notepad}}}}~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} opens a proof state
    3.31 +  without any goal statement.  This allows to experiment with Isar,
    3.32 +  without producing any persistent result.
    3.33  
    3.34 -  Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
    3.35 -  followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'', which means the
    3.36 -  example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
    3.37 -  discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    3.38 +  The notepad can be closed by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} or discontinued by
    3.39 +  \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
    3.40  
    3.41    \end{description}%
    3.42  \end{isamarkuptext}%
     4.1 --- a/etc/isar-keywords-ZF.el	Sun Dec 05 13:42:58 2010 +0100
     4.2 +++ b/etc/isar-keywords-ZF.el	Sun Dec 05 14:02:16 2010 +0100
     4.3 @@ -61,7 +61,6 @@
     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 @@ -415,7 +414,6 @@
    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	Sun Dec 05 13:42:58 2010 +0100
     5.2 +++ b/etc/isar-keywords.el	Sun Dec 05 14:02:16 2010 +0100
     5.3 @@ -86,7 +86,6 @@
     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 @@ -533,7 +532,6 @@
    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	Sun Dec 05 13:42:58 2010 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Dec 05 14:02:16 2010 +0100
     6.3 @@ -513,13 +513,6 @@
     6.4      (Parse.begin >> K Proof.begin_notepad);
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.local_theory_to_proof "example_proof"
     6.8 -    "example proof body, without any result" Keyword.thy_schematic_goal
     6.9 -    (Scan.succeed
    6.10 -      (Specification.theorem_cmd "" NONE (K I)
    6.11 -        Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
    6.12 -
    6.13 -val _ =
    6.14    Outer_Syntax.command "have" "state local goal"
    6.15      (Keyword.tag_proof Keyword.prf_goal)
    6.16      (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));