# 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 \ - @@{command theory} @{syntax name} imports? \ keywords? abbrevs? @'begin' - ; - imports: @'imports' (@{syntax name} +) + @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \ + keywords? abbrevs? @'begin' ; keywords: @'keywords' (keyword_decls + @'and') ;