diff -r 5467858e9419 -r f6c88cb715db src/Doc/Isar_Ref/Document_Preparation.thy
--- 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.