equal
deleted
inserted
replaced
154 |
154 |
155 text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions} |
155 text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions} |
156 Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as |
156 Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as |
157 simplification rules, but by default they are not: the simplifier does not |
157 simplification rules, but by default they are not: the simplifier does not |
158 expand them automatically. Definitions are intended for introducing abstract |
158 expand them automatically. Definitions are intended for introducing abstract |
159 concepts and not merely as abbreviations. (Contrast with syntax |
159 concepts and not merely as abbreviations. Of course, we need to expand |
160 translations, \S\ref{sec:def-translations}.) Of course, we need to expand |
|
161 the definition initially, but once we have proved enough abstract properties |
160 the definition initially, but once we have proved enough abstract properties |
162 of the new constant, we can forget its original definition. This style makes |
161 of the new constant, we can forget its original definition. This style makes |
163 proofs more robust: if the definition has to be changed, |
162 proofs more robust: if the definition has to be changed, |
164 only the proofs of the abstract properties will be affected. |
163 only the proofs of the abstract properties will be affected. |
165 |
164 |