diff -r 18f90044c777 -r ec47352e99c2 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Thu Mar 12 14:25:35 2009 +0000 +++ b/CookBook/Tactical.thy Thu Mar 12 15:43:22 2009 +0000 @@ -2033,10 +2033,11 @@ the same assumptions as in \ref{ex:addsimproc}. \end{exercise} - \begin{exercise} - Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of - rewriting such terms is faster. For this you might have to construct quite - large terms. Also see Recipe \ref{rec:timing} for information about timing. + \begin{exercise}\label{ex:compare} + Compare your solutions of Exercises~\ref{addsimproc} and \ref{ex:addconversion}, + and try to determine which way of rewriting such terms is faster. For this you might + have to construct quite large terms. Also see Recipe \ref{rec:timing} for information + about timing. \end{exercise} \begin{readmore}