1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 06 21:06:17 2011 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 06 21:06:18 2011 +0100
     1.3 @@ -497,6 +497,7 @@
     1.4      @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     1.5      @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
     1.6      @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     1.7 +    @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.8      @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.9    \end{matharray}
    1.10  
    1.11 @@ -508,10 +509,12 @@
    1.12      ;
    1.13      'sublocale' nameref ('<' | subseteq) localeexpr equations?
    1.14      ;
    1.15 -    equations: 'where' (thmdecl? prop + 'and')
    1.16 +    'print_dependencies' '!'? localeexpr
    1.17      ;
    1.18      'print_interps' nameref
    1.19      ;
    1.20 +    equations: 'where' (thmdecl? prop + 'and')
    1.21 +    ;
    1.22    \end{rail}
    1.23  
    1.24    \begin{description}
    1.25 @@ -580,6 +583,14 @@
    1.26    from the interpreted locales to entities of @{text name}.  This
    1.27    feature is experimental.
    1.28  
    1.29 +  \item @{command "print_dependencies"}~@{text "expr"} is useful for
    1.30 +  understanding the effect of an interpretation of @{text "expr"}.  It
    1.31 +  lists all locale instances for which interpretations would be added
    1.32 +  to the current context.  Variant @{command
    1.33 +  "print_dependencies"}@{text "!"} prints all locale instances that
    1.34 +  would be considered for interpretation, and would be interpreted in
    1.35 +  an empty context (that is, without interpretations).
    1.36 +
    1.37    \item @{command "print_interps"}~@{text "locale"} lists all
    1.38    interpretations of @{text "locale"} in the current theory or proof
    1.39    context, including those due to a combination of a @{command