doc-src/IsarRef/syntax.tex
changeset 8690 48786b52c8d8
parent 8593 68619606c5d1
child 8896 c80aba8c1d5e
equal deleted inserted replaced
8689:a2e82eed6454 8690:48786b52c8d8
   176   ;
   176   ;
   177   prop: term
   177   prop: term
   178   ;
   178   ;
   179 \end{rail}
   179 \end{rail}
   180 
   180 
       
   181 Positional instantiations are indicated by giving a sequence of terms, or the
       
   182 placeholder ``$\_$'' (underscore), which means to skip a position.
       
   183 
       
   184 \indexoutertoken{inst}\indexoutertoken{insts}
       
   185 \begin{rail}
       
   186   inst: underscore | term
       
   187   ;
       
   188   insts: (inst *)
       
   189   ;
       
   190 \end{rail}
       
   191 
   181 Type declarations and definitions usually refer to \railnonterm{typespec} on
   192 Type declarations and definitions usually refer to \railnonterm{typespec} on
   182 the left-hand side.  This models basic type constructor application at the
   193 the left-hand side.  This models basic type constructor application at the
   183 outer syntax level.  Note that only plain postfix notation is available here,
   194 outer syntax level.  Note that only plain postfix notation is available here,
   184 but no infixes.
   195 but no infixes.
   185 
   196