--- 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}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 22 09:04:45 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 22 09:04:45 2009 +0100
@@ -453,7 +453,6 @@
\begin{matharray}{rcl}
\indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
- \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\end{matharray}
\indexouternonterm{interp}
@@ -462,8 +461,6 @@
;
'interpret' interp
;
- 'print\_interps' '!'? name
- ;
instantiation: ('[' (inst+) ']')?
;
interp: (name ':')? \\ (contextexpr instantiation |
@@ -543,13 +540,6 @@
interprets \isa{expr} in the proof context and is otherwise
similar to interpretation in theories.
- \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc} prints the
- interpretations of a particular locale \isa{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}