diff -r b044a06ad0d6 -r d997c7ba3305 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Aug 23 21:08:27 2019 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Aug 24 12:03:00 2019 +0200
@@ -501,7 +501,7 @@
 subsection \<open>Locale declarations\<close>
 
 text \<open>
-  \begin{matharray}{rcl}
+  \begin{tabular}{rcll}
     @{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
     @{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
     @{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@@ -509,7 +509,8 @@
     @{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{method_def intro_locales} & : & \<open>method\<close> \\
     @{method_def unfold_locales} & : & \<open>method\<close> \\
-  \end{matharray}
+    @{attribute_def trace_locales} & : & \<open>attribute\<close> & default \<open>false\<close> \\
+  \end{tabular}
 
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
@@ -627,6 +628,11 @@
   specifications entailed by the context, both from target statements, and
   from interpretations (see below). New goals that are entailed by the current
   context are discharged automatically.
+
+  \<^descr> @{attribute trace_locales}, when set to
+  \<open>true\<close>, prints the locale instances activated during
+  roundup.  Useful for understanding local theories created by complex
+  locale hierarchies.
 \<close>