--- 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}