more accurate diagram;
authorwenzelm
Fri, 25 May 2018 21:00:47 +0200
changeset 68272 ddeb6847451a
parent 68271 77f6fa78b6e1
child 68273 53788963c4dc
more accurate diagram;
src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri May 25 13:47:58 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri May 25 21:00:47 2018 +0200
@@ -281,12 +281,14 @@
     @{syntax_def mixfix}: '('
       (@{syntax template} prios? @{syntax nat}? |
         (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
-        @'binder' @{syntax template} prios? @{syntax nat} |
+        @'binder' @{syntax template} prio? @{syntax nat} |
         @'structure') ')'
     ;
     @{syntax template}: string
     ;
     prios: '[' (@{syntax nat} + ',') ']'
+    ;
+    prio: '[' @{syntax nat} ']'
   \<close>}
 
   The string given as \<open>template\<close> may include literal text, spacing, blocks,