diff -r 41a802bbb7df -r 0a567f923b42 ProgTutorial/FirstSteps.thy --- 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