equal
deleted
inserted
replaced
172 ; |
172 ; |
173 \end{rail} |
173 \end{rail} |
174 |
174 |
175 \begin{descr} |
175 \begin{descr} |
176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the |
176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the |
177 induction rule of the type/set/function specified by $kind$ and instantiated |
177 induction rule of the type~/ set~/ function specified by $kind$ and |
178 by $insts$. The latter either consists of pairs $P$ $x$ (induction |
178 instantiated by $insts$. The latter either consists of pairs $P$ $x$ |
179 predicate and variable), where $P$ is optional. If $kind$ is omitted, the |
179 (induction predicate and variable), where $P$ is optional. If $kind$ is |
180 default is to pick a datatype induction rule according to the type of some |
180 omitted, the default is to pick a datatype induction rule according to the |
181 induction variable, which may not be omitted that case. |
181 type of some induction variable, which may not be omitted that case. |
182 \end{descr} |
182 \end{descr} |
183 |
183 |
184 |
184 |
185 \section{Arithmetic} |
185 \section{Arithmetic} |
186 |
186 |