ProgTutorial/FirstSteps.thy
changeset 293 0a567f923b42
parent 292 41a802bbb7df
child 298 8057d65607eb
--- 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