equal
deleted
inserted
replaced
164 \begin{isamarkuptext}% |
164 \begin{isamarkuptext}% |
165 \noindent |
165 \noindent |
166 Of course we can also unfold definitions in the middle of a proof. |
166 Of course we can also unfold definitions in the middle of a proof. |
167 |
167 |
168 You should normally not turn a definition permanently into a simplification |
168 You should normally not turn a definition permanently into a simplification |
169 rule because this defeats the whole purpose of an abbreviation. |
169 rule because this defeats the whole purpose. |
170 |
170 |
171 \begin{warn} |
171 \begin{warn} |
172 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold |
172 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold |
173 occurrences of $f$ with at least two arguments. This may be helpful for unfolding |
173 occurrences of $f$ with at least two arguments. This may be helpful for unfolding |
174 $f$ selectively, but it may also get in the way. Defining |
174 $f$ selectively, but it may also get in the way. Defining |