# HG changeset patch
# User wenzelm
# Date 1192055623 -7200
# Node ID 3bf6915081d943330c6285cac0f28017461598e5
# Parent  0664f10a4094b247cd5b7e32eea273f676b76db7
'notation': allow structmixfix;

diff -r 0664f10a4094 -r 3bf6915081d9 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Oct 11 00:28:32 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu Oct 11 00:33:43 2007 +0200
@@ -31,7 +31,7 @@
   ;
   'abbreviation' target? mode? (decl 'where')? prop
   ;
-  ('notation' | 'no\_notation') target? mode? (nameref mixfix + 'and')
+  ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
   ;
 
   fixes: ((name ('::' type)? mixfix? | vars) + 'and')
@@ -94,8 +94,8 @@
   representation of the given entity is retrieved from the context.
   
 \item $\isarkeyword{no_notation}$ is similar to
-$\isarkeyword{notation}$, but removes the specified syntax annotation
-from the present context.
+  $\isarkeyword{notation}$, but removes the specified syntax
+  annotation from the present context.
 
 \end{descr}