diff -r c15bcd87f47c -r dd58f13a8eb4 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:54 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:55 2006 +0100
@@ -29,7 +29,7 @@
   ;
   'abbreviation' target? mode? (constdecl? prop +)
   ;
-  'notation' target? mode? (nameref mixfix +)
+  'notation' target? mode? (nameref mixfix + 'and')
   ;
 
   consts: ((name ('::' type)? structmixfix? | vars) + 'and')