diff -r 9ec4482c9201 -r f5d79aeffd81 doc-src/IsarRef/Thy/Misc.thy
--- 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 {*