--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Jul 02 12:39:08 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Jul 02 14:09:43 2015 +0200
@@ -438,6 +438,9 @@
@{rail \<open>
@{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
;
+ @{syntax_def thmbind}:
+ @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
+ ;
@{syntax_def thmdecl}: thmbind ':'
;
@{syntax_def thmdef}: thmbind '='
@@ -449,9 +452,6 @@
;
@{syntax_def thmrefs}: @{syntax thmref} +
;
-
- thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
- ;
selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
\<close>}
\<close>