equal
deleted
inserted
replaced
2031 \ref{ex:addsimproc}, but is based in conversions. That means replace terms |
2031 \ref{ex:addsimproc}, but is based in conversions. That means replace terms |
2032 of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make |
2032 of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make |
2033 the same assumptions as in \ref{ex:addsimproc}. |
2033 the same assumptions as in \ref{ex:addsimproc}. |
2034 \end{exercise} |
2034 \end{exercise} |
2035 |
2035 |
2036 \begin{exercise} |
2036 \begin{exercise}\label{ex:compare} |
2037 Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of |
2037 Compare your solutions of Exercises~\ref{addsimproc} and \ref{ex:addconversion}, |
2038 rewriting such terms is faster. For this you might have to construct quite |
2038 and try to determine which way of rewriting such terms is faster. For this you might |
2039 large terms. Also see Recipe \ref{rec:timing} for information about timing. |
2039 have to construct quite large terms. Also see Recipe \ref{rec:timing} for information |
|
2040 about timing. |
2040 \end{exercise} |
2041 \end{exercise} |
2041 |
2042 |
2042 \begin{readmore} |
2043 \begin{readmore} |
2043 See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. |
2044 See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. |
2044 Further conversions are defined in @{ML_file "Pure/thm.ML"}, |
2045 Further conversions are defined in @{ML_file "Pure/thm.ML"}, |