doc-src/Intro/advanced.tex
changeset 1185 9968989790e2
parent 1084 502a61cbf37b
child 1366 3f3c25d3ec04
equal deleted inserted replaced
1184:94ada3b54caa 1185:9968989790e2
   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 translations {\it translation declarations}
   342 defs         {\it constant definitions}
   342 defs         {\it definitions}
   343 rules        {\it rule declarations}
   343 rules        {\it rule declarations}
   344 end
   344 end
   345 ML           {\it ML code}
   345 ML           {\it ML code}
   346 \end{ttbox}
   346 \end{ttbox}
   347 This declares the theory $T$ to extend the existing theories
   347 This declares the theory $T$ to extend the existing theories