doc-src/IsarRef/syntax.tex
changeset 8896 c80aba8c1d5e
parent 8690 48786b52c8d8
child 9051 887a15590f0e
     1.1 --- a/doc-src/IsarRef/syntax.tex	Sun May 21 14:32:47 2000 +0200
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Sun May 21 14:33:46 2000 +0200
     1.3 @@ -139,15 +139,17 @@
     1.4  
     1.5  \subsection{Type classes, sorts and arities}
     1.6  
     1.7 -The syntax of sorts and arities is given directly at the outer level.  Note
     1.8 -that this is in contrast to types and terms (see \ref{sec:types-terms}).
     1.9 +Classes are specified by plain names.  Sorts have a very simple inner syntax,
    1.10 +which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
    1.11 +referring to the intersection of these classes.  The syntax of type arities is
    1.12 +given directly at the outer level.
    1.13  
    1.14  \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
    1.15  \indexouternonterm{classdecl}
    1.16  \begin{rail}
    1.17    classdecl: name ('<' (nameref + ','))?
    1.18    ;
    1.19 -  sort: nameref | lbrace (nameref * ',') rbrace
    1.20 +  sort: nameref
    1.21    ;
    1.22    arity: ('(' (sort + ',') ')')? sort
    1.23    ;
    1.24 @@ -252,7 +254,7 @@
    1.25  \begin{rail}
    1.26    atom: nameref | typefree | typevar | var | nat | keyword
    1.27    ;
    1.28 -  arg: atom | '(' args ')' | '[' args ']' | lbrace args rbrace
    1.29 +  arg: atom | '(' args ')' | '[' args ']'
    1.30    ;
    1.31    args: arg *
    1.32    ;