src/Doc/Isar_Ref/Outer_Syntax.thy

--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 25 11:40:58 2017 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 25 13:47:53 2017 +0200
@@ -188,6 +188,9 @@
     ;
     @{syntax_def par_name}: '(' @{syntax name} ')'
   \<close>}
+
+  A @{syntax_def system_name} is like @{syntax name}, but it excludes
+  white-space characters and needs to conform to file-name notation.
 \<close>