--- a/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:45:40 2008 +0100
+++ b/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:48:19 2008 +0100
@@ -6,95 +6,6 @@
chapter {* Other commands \label{ch:pure-syntax} *}
-section {* Diagnostics *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
- @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- \end{matharray}
-
- These diagnostic commands assist interactive development. Note that
- @{command undo} does not apply here, the theory or proof
- configuration is not changed.
-
- \begin{rail}
- 'pr' modes? nat? (',' nat)?
- ;
- 'thm' modes? thmrefs
- ;
- 'term' modes? term
- ;
- 'prop' modes? prop
- ;
- 'typ' modes? type
- ;
- 'prf' modes? thmrefs?
- ;
- 'full\_prf' modes? thmrefs?
- ;
-
- modes: '(' (name + ) ')'
- ;
- \end{rail}
-
- \begin{description}
-
- \item @{command "pr"}~@{text "goals, prems"} prints the current
- proof state (if present), including the proof context, current facts
- and goals. The optional limit arguments affect the number of goals
- and premises to be displayed, which is initially 10 for both.
- Omitting limit values leaves the current setting unchanged.
-
- \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
- theorems from the current theory or proof context. Note that any
- attributes included in the theorem specifications are applied to a
- temporary context derived from the current theory or proof; the
- result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
- \<dots>, a\<^sub>n"} do not have any permanent effect.
-
- \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
- read, type-check and print terms or propositions according to the
- current theory or proof context; the inferred type of @{text t} is
- output as well. Note that these commands are also useful in
- inspecting the current environment of term abbreviations.
-
- \item @{command "typ"}~@{text \<tau>} reads and prints types of the
- meta-logic according to the current theory or proof context.
-
- \item @{command "prf"} displays the (compact) proof term of the
- current proof state (if present), or of the given theorems. Note
- that this requires proof terms to be switched on for the current
- object logic (see the ``Proof terms'' section of the Isabelle
- reference manual for information on how to do this).
-
- \item @{command "full_prf"} is like @{command "prf"}, but displays
- the full proof term, i.e.\ also displays information omitted in the
- compact proof term, which is denoted by ``@{text _}'' placeholders
- there.
-
- \end{description}
-
- All of the diagnostic commands above admit a list of @{text modes}
- to be specified, which is appended to the current print mode (see
- also \cite{isabelle-ref}). Thus the output behavior may be modified
- according particular print mode features. For example, @{command
- "pr"}~@{text "(latex xsymbols symbols)"} would print the current
- proof state with mathematical symbols and special characters
- represented in {\LaTeX} source, according to the Isabelle style
- \cite{isabelle-sys}.
-
- Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
- systematic way to include formal items into the printed text
- document.
-*}
-
-
section {* Inspecting the context *}
text {*