diff -r 8cfd585b9162 -r e04c44dc11fc src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Fri Jan 04 12:33:25 2013 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Fri Jan 04 12:44:47 2013 +0100
@@ -459,6 +459,7 @@
     @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{method_def intro_locales} & : & @{text method} \\
     @{method_def unfold_locales} & : & @{text method} \\
   \end{matharray}
@@ -572,6 +573,10 @@
   \item @{command "print_locales"} prints the names of all locales
   of the current theory.
 
+  \item @{command "locale_deps"} visualizes all locales and their
+  relations as a Hasse diagram. This includes locales defined as type
+  classes (\secref{sec:class}).
+
   \item @{method intro_locales} and @{method unfold_locales}
   repeatedly expand all introduction rules of locale predicates of the
   theory.  While @{method intro_locales} only applies the @{text