equal
deleted
inserted
replaced
110 \item[$trans$] |
110 \item[$trans$] |
111 specifies syntactic translation rules (macros). There are three forms: |
111 specifies syntactic translation rules (macros). There are three forms: |
112 parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt |
112 parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt |
113 ==}). |
113 ==}). |
114 |
114 |
115 \item[$rule$] |
115 \item[$rules$] |
116 is a series of rule declarations. Each has a name $id$ and the formula is |
116 is a series of rule declarations. Each has a name $id$ and the formula is |
117 given by the $string$. Rule names must be distinct within any single |
117 given by the $string$. Rule names must be distinct within any single |
118 theory file. |
118 theory file. |
|
119 |
|
120 \item[$defs$] |
|
121 is a series of definitions. Just like $rules$, except that every $string$ |
|
122 must be a definition. |
|
123 |
|
124 \item[$constdefs$] combines the declaration of constants and their |
|
125 definition. The first $string$ is the type, the second the definition. |
119 |
126 |
120 \item[$ml$] \index{*ML section} |
127 \item[$ml$] \index{*ML section} |
121 consists of \ML\ code, typically for parse and print translation functions. |
128 consists of \ML\ code, typically for parse and print translation functions. |
122 \end{description} |
129 \end{description} |
123 % |
130 % |