clarified index, more like formal @{element_ref};
authorwenzelm
Sun, 23 May 2021 19:59:37 +0200
changeset 74026 1419cb7f7f3e
parent 74025 08db0a06e131
child 74027 d07ab5b14453
clarified index, more like formal @{element_ref};
src/Doc/Isar_Ref/Spec.thy
--- 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'?
     ;