changeset 841 14b96e3bd4ab parent 459 03b445551763 child 1084 502a61cbf37b
equal inserted replaced
840:5716e174b591 841:14b96e3bd4ab
   336 classes      {\it class declarations}
   336 classes      {\it class declarations}
   337 default      {\it sort}
   337 default      {\it sort}
   338 types        {\it type declarations and synonyms}
   338 types        {\it type declarations and synonyms}
   339 arities      {\it arity declarations}
   339 arities      {\it arity declarations}
   340 consts       {\it constant declarations}
   340 consts       {\it constant declarations}

   341 translations {\it translation declarations}
   341 rules        {\it rule declarations}
   342 rules        {\it rule declarations}
   343 end
   343 end
   344 ML           {\it ML code}
   344 ML           {\it ML code}
   345 \end{ttbox}
   345 \end{ttbox}
   346 This declares the theory $T$ to extend the existing theories
   346 This declares the theory $T$ to extend the existing theories
   347 $S@1$,~\ldots,~$S@n$.  It may declare new classes, types, arities
   347 $S@1$,~\ldots,~$S@n$.  It may declare new classes, types, arities
   451
   451
   452 The {\bf type declaration part} has the general form
   452 The {\bf type declaration part} has the general form
   453 \begin{ttbox}
   453 \begin{ttbox}
   454 types   $$tids@1$$ $$id@1$$
   454 types   $$tids@1$$ $$id@1$$
   455         \vdots
   455         \vdots
   456         $$tids@1$$ $$id@n$$
   456         $$tids@n$$ $$id@n$$
   457 \end{ttbox}
   457 \end{ttbox}
   458 where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
   458 where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
   459 are type argument lists as shown in the example above.  It declares each
   459 are type argument lists as shown in the example above.  It declares each
   460 $id@i$ as a type constructor with the specified number of argument places.
   460 $id@i$ as a type constructor with the specified number of argument places.
   461
   461