equal
deleted
inserted
replaced
1169 \begin{readmore} |
1169 \begin{readmore} |
1170 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1170 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1171 the file @{ML_file "Pure/thm.ML"}. |
1171 the file @{ML_file "Pure/thm.ML"}. |
1172 \end{readmore} |
1172 \end{readmore} |
1173 |
1173 |
1174 \begin{exercise} |
1174 \begin{exercise}\label{fun:revsum typed} |
1175 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
1175 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
1176 result that type-checks. |
1176 result that type-checks. |
1177 \end{exercise} |
1177 \end{exercise} |
1178 |
1178 |
1179 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1179 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |