src/Doc/Isar_Ref/Outer_Syntax.thy

 
   @{rail \<open>
     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
     ;
     @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
+    ;
+    @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +)
   \<close>}
 
   The treatment of multiple declarations corresponds to the
   complementary focus of @{syntax vars} versus @{syntax props}.  In
   ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the typing refers to all variables, while