--- a/ProgTutorial/FirstSteps.thy Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Tue Jul 28 12:11:33 2009 +0200
@@ -1218,9 +1218,11 @@
the file @{ML_file "Pure/thm.ML"}.
\end{readmore}
- \begin{exercise}\label{fun:revsum typed}
+ \begin{exercise}
Check that the function defined in Exercise~\ref{fun:revsum} returns a
- result that type-checks.
+ result that type-checks. See what happens to the solutions of this
+ exercise given in \ref{ch:solutions} when they receive an ill-typed term
+ as input.
\end{exercise}
Remember Isabelle follows the Church-style typing for terms, i.e., a term contains