# HG changeset patch
# User haftmann
# Date 1232611485 -3600
# Node ID 595d91e50510849f657340ce168cacd4720af677
# Parent  4f68e0f8f4fd8c988e8fc4e40da17d90c86a474f
dropped print_interps

diff -r 4f68e0f8f4fd -r 595d91e50510 doc-src/IsarRef/Thy/Spec.thy
--- 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}
diff -r 4f68e0f8f4fd -r 595d91e50510 doc-src/IsarRef/Thy/document/Spec.tex
--- 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}