# HG changeset patch
# User wenzelm
# Date 955575901 -7200
# Node ID 48786b52c8d8e46060a7938ad9568c0791463a4a
# Parent  a2e82eed6454e65d4fb9885701a2a0ffd320eec7
added inst, insts;

diff -r a2e82eed6454 -r 48786b52c8d8 doc-src/IsarRef/syntax.tex
--- 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,