1.1 --- a/doc-src/Ref/defining.tex	Mon Sep 22 17:35:52 1997 +0200
     1.2 +++ b/doc-src/Ref/defining.tex	Mon Sep 22 17:37:03 1997 +0200
     1.3 @@ -104,10 +104,12 @@
     1.4        &$|$& $logic^{(4)}$ {\tt::} $type$ & (3) \\
     1.5        &$|$& $id$ ~~$|$~~ $var$
     1.6      ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\
     1.7 -      &$|$& {\tt \%} $idts$ {\tt.} $any^{(3)}$ & (3) \\\\
     1.8 +      &$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\\\
     1.9  $idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
    1.10  $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
    1.11      &$|$& $id$ {\tt ::} $type$ & (0) \\\\
    1.12 +$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\
    1.13 +$pttrn$ &=& $idt$ \\\\
    1.14  $type$ &=& {\tt(} $type$ {\tt)} \\
    1.15       &$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
    1.16         ~~$|$~~ $tvar$ {\tt::} $sort$ \\
    1.17 @@ -164,6 +166,10 @@
    1.18  
    1.19    \item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained
    1.20      by types.
    1.21 +    
    1.22 +  \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
    1.23 +    abstraction, cases etc.  Initially the same as $idt$ and $idts$,
    1.24 +    these are indetended to be augmented by user extensions.
    1.25  
    1.26    \item[\ndxbold{type}] denotes types of the meta-logic.
    1.27