# HG changeset patch
# User wenzelm
# Date 1470152378 -7200
# Node ID 7f06347a5013641d72aedc34eff930d4d4f5ecad
# Parent  73939a9b70a3f100ef24d16cfb172cbc68ee8568
clarified: 'imports' is de-facto mandatory;

diff -r 73939a9b70a3 -r 7f06347a5013 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 17:35:18 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 17:39:38 2016 +0200
@@ -58,9 +58,8 @@
   such a global @{command (global) "end"}.
 
   @{rail \<open>
-    @@{command theory} @{syntax name} imports? \<newline> keywords? abbrevs? @'begin'
-    ;
-    imports: @'imports' (@{syntax name} +)
+    @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \<newline>
+      keywords? abbrevs? @'begin'
     ;
     keywords: @'keywords' (keyword_decls + @'and')
     ;