equal
deleted
inserted
replaced
1216 \begin{readmore} |
1216 \begin{readmore} |
1217 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1217 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1218 the file @{ML_file "Pure/thm.ML"}. |
1218 the file @{ML_file "Pure/thm.ML"}. |
1219 \end{readmore} |
1219 \end{readmore} |
1220 |
1220 |
1221 \begin{exercise}\label{fun:revsum typed} |
1221 \begin{exercise} |
1222 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
1222 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
1223 result that type-checks. |
1223 result that type-checks. See what happens to the solutions of this |
|
1224 exercise given in \ref{ch:solutions} when they receive an ill-typed term |
|
1225 as input. |
1224 \end{exercise} |
1226 \end{exercise} |
1225 |
1227 |
1226 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1228 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1227 enough typing information (constants, free variables and abstractions all have typing |
1229 enough typing information (constants, free variables and abstractions all have typing |
1228 information) so that it is always clear what the type of a term is. |
1230 information) so that it is always clear what the type of a term is. |