equal
deleted
inserted
replaced
2309 in |
2309 in |
2310 More_Conv.bottom_conv (K conv) ctxt |
2310 More_Conv.bottom_conv (K conv) ctxt |
2311 end*} |
2311 end*} |
2312 |
2312 |
2313 text {* |
2313 text {* |
2314 The function @{ML bottom_conv in More_Conv} traverses first the the term and |
2314 If we regard terms as trees with variables and constants on the top, then |
|
2315 @{ML bottom_conv in More_Conv} traverses first the the term and |
2315 on the ``way down'' applies the conversion, whereas @{ML top_conv in |
2316 on the ``way down'' applies the conversion, whereas @{ML top_conv in |
2316 More_Conv} applies the conversion on the ``way up''. To see the difference, |
2317 More_Conv} applies the conversion on the ``way up''. To see the difference, |
2317 assume the following two meta-equations. |
2318 assume the following two meta-equations. |
2318 *} |
2319 *} |
2319 |
2320 |