CookBook/Tactical.thy
changeset 172 ec47352e99c2
parent 170 90bee31628dc
child 173 d820cb5873ea
--- 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}