--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Aug 25 20:48:16 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sat Aug 25 21:15:43 2018 +0200
@@ -94,6 +94,7 @@
@{antiquotation_def typ} & : & \<open>antiquotation\<close> \\
@{antiquotation_def type} & : & \<open>antiquotation\<close> \\
@{antiquotation_def class} & : & \<open>antiquotation\<close> \\
+ @{antiquotation_def locale} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "text"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def goals} & : & \<open>antiquotation\<close> \\
@{antiquotation_def subgoals} & : & \<open>antiquotation\<close> \\
@@ -180,6 +181,7 @@
@@{antiquotation typ} options @{syntax type} |
@@{antiquotation type} options @{syntax embedded} |
@@{antiquotation class} options @{syntax embedded} |
+ @@{antiquotation locale} options @{syntax embedded} |
(@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
options @{syntax name}
;
@@ -252,6 +254,8 @@
\<^descr> \<open>@{class c}\<close> prints a class \<open>c\<close>.
+ \<^descr> \<open>@{locale c}\<close> prints a locale \<open>c\<close>.
+
\<^descr> \<open>@{command name}\<close>, \<open>@{method name}\<close>, \<open>@{attribute name}\<close> print checked
entities of the Isar language.