--- a/doc-src/IsarRef/syntax.tex Wed Apr 12 18:53:20 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex Wed Apr 12 23:45:01 2000 +0200
@@ -178,6 +178,17 @@
;
\end{rail}
+Positional instantiations are indicated by giving a sequence of terms, or the
+placeholder ``$\_$'' (underscore), which means to skip a position.
+
+\indexoutertoken{inst}\indexoutertoken{insts}
+\begin{rail}
+ inst: underscore | term
+ ;
+ insts: (inst *)
+ ;
+\end{rail}
+
Type declarations and definitions usually refer to \railnonterm{typespec} on
the left-hand side. This models basic type constructor application at the
outer syntax level. Note that only plain postfix notation is available here,