# HG changeset patch
# User wenzelm
# Date 1328361639 -3600
# Node ID 30953ef09bcd50d043cfe5e945773b0098efbea1
# Parent  6233d0b74d71b5829686c1a4e232728f091c54f9
simplified mixfix (NB: infix is no longer required separately);

diff -r 6233d0b74d71 -r 30953ef09bcd doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Feb 02 21:21:41 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 14:20:39 2012 +0100
@@ -339,11 +339,10 @@
   annotations.
 
   @{rail "
-    @{syntax_def \"infix\"}: '(' (@'infix' | @'infixl' | @'infixr')
-      @{syntax string} @{syntax nat} ')'
-    ;
-    @{syntax_def mixfix}: @{syntax \"infix\"} | '(' @{syntax string} prios? @{syntax nat}? ')' |
-    '(' @'binder' @{syntax string} prios? @{syntax nat} ')'
+    @{syntax_def mixfix}: '(' (
+      @{syntax string} prios? @{syntax nat}? |
+      (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} |
+      @'binder' @{syntax string} prios? @{syntax nat} ) ')'
     ;
     @{syntax_def struct_mixfix}: @{syntax mixfix} | '(' @'structure' ')'
     ;
diff -r 6233d0b74d71 -r 30953ef09bcd doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 02 21:21:41 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Feb 04 14:20:39 2012 +0100
@@ -416,45 +416,38 @@
   annotations.
 
   \begin{railoutput}
-\rail@begin{3}{\indexdef{}{syntax}{infix}\hypertarget{syntax.infix}{\hyperlink{syntax.infix}{\mbox{\isa{infix}}}}}
+\rail@begin{7}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@bar
+\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{prios}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@nextbar{2}
+\rail@bar
 \rail@term{\isa{\isakeyword{infix}}}[]
-\rail@nextbar{1}
+\rail@nextbar{3}
 \rail@term{\isa{\isakeyword{infixl}}}[]
-\rail@nextbar{2}
+\rail@nextbar{4}
 \rail@term{\isa{\isakeyword{infixr}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{5}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
-\rail@bar
-\rail@nont{\hyperlink{syntax.infix}{\mbox{\isa{infix}}}}[]
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@nextbar{5}
+\rail@term{\isa{\isakeyword{binder}}}[]
 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
 \rail@bar
-\rail@nextbar{2}
+\rail@nextbar{6}
 \rail@nont{\isa{prios}}[]
 \rail@endbar
-\rail@bar
-\rail@nextbar{2}
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
 \rail@endbar
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@nextbar{3}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{\isakeyword{binder}}}[]
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
-\rail@bar
-\rail@nextbar{4}
-\rail@nont{\isa{prios}}[]
-\rail@endbar
-\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
 \rail@end
 \rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
 \rail@bar