--- a/doc-src/IsarRef/Thy/Spec.thy Thu Jan 22 09:04:45 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Jan 22 09:04:45 2009 +0100
@@ -436,7 +436,6 @@
\begin{matharray}{rcl}
@{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
@{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
- @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
\indexouternonterm{interp}
@@ -445,8 +444,6 @@
;
'interpret' interp
;
- 'print\_interps' '!'? name
- ;
instantiation: ('[' (inst+) ']')?
;
interp: (name ':')? \\ (contextexpr instantiation |
@@ -531,13 +528,6 @@
interprets @{text expr} in the proof context and is otherwise
similar to interpretation in theories.
- \item @{command "print_interps"}~@{text loc} prints the
- interpretations of a particular locale @{text loc} that are active
- in the current context, either theory or proof context. The
- exclamation point argument triggers printing of \emph{witness}
- theorems justifying interpretations. These are normally omitted
- from the output.
-
\end{description}
\begin{warn}