equal
deleted
inserted
replaced
1 theory Solutions |
1 theory Solutions |
2 imports Base "Recipes/Timing" |
2 imports FirstSteps "Recipes/Timing" |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
5 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
6 |
6 |
7 text {* \solution{fun:revsum} *} |
7 text {* \solution{fun:revsum} *} |
286 |
286 |
287 text {* |
287 text {* |
288 This function generates for example: |
288 This function generates for example: |
289 |
289 |
290 @{ML_response_fake [display,gray] |
290 @{ML_response_fake [display,gray] |
291 "writeln (Syntax.string_of_term @{context} (term_tree 2))" |
291 "writeln (string_of_term @{context} (term_tree 2))" |
292 "(1 + 2) + (3 + 4)"} |
292 "(1 + 2) + (3 + 4)"} |
293 |
293 |
294 The next function constructs a goal of the form @{text "P \<dots>"} with a term |
294 The next function constructs a goal of the form @{text "P \<dots>"} with a term |
295 produced by @{ML term_tree} filled in. |
295 produced by @{ML term_tree} filled in. |
296 *} |
296 *} |