--- a/src/Doc/Isar_Ref/Spec.thy Sun May 23 19:29:18 2021 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sun May 23 19:59:37 2021 +0200
@@ -520,11 +520,11 @@
@{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{tabular}
- @{index_ref \<open>\<^theory_text>\<open>fixes\<close>\<close>}
- @{index_ref \<open>\<^theory_text>\<open>constrains\<close>\<close>}
- @{index_ref \<open>\<^theory_text>\<open>assumes\<close>\<close>}
- @{index_ref \<open>\<^theory_text>\<open>defines\<close>\<close>}
- @{index_ref \<open>\<^theory_text>\<open>notes\<close>\<close>}
+ @{index_ref \<open>\<^theory_text>\<open>fixes\<close> (element)\<close>}
+ @{index_ref \<open>\<^theory_text>\<open>constrains\<close> (element)\<close>}
+ @{index_ref \<open>\<^theory_text>\<open>assumes\<close> (element)\<close>}
+ @{index_ref \<open>\<^theory_text>\<open>defines\<close> (element)\<close>}
+ @{index_ref \<open>\<^theory_text>\<open>notes\<close> (element)\<close>}
\<^rail>\<open>
@@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
;