--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Fri Mar 19 00:46:08 2010 +0100
@@ -320,9 +320,13 @@
only plain postfix notation is available here, but no infixes.
\indexouternonterm{typespec}
+ \indexouternonterm{typespecsorts}
\begin{rail}
typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
;
+
+ typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
+ ;
\end{rail}%
\end{isamarkuptext}%
\isamarkuptrue%