src/Doc/Isar_Ref/Document_Preparation.thy
changeset 62912 745d31e63c21
parent 62274 199f4d6dab0a
child 62965 5bf08c9aa036
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 07 21:39:03 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 07 22:09:23 2016 +0200
@@ -49,8 +49,9 @@
 
   @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
-      @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph} |
-      @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
+      @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph})
+      @{syntax text} ';'? |
+    (@@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
   \<close>}
 
     \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark