equal
deleted
inserted
replaced
303 |
303 |
304 text {* |
304 text {* |
305 This function generates for example: |
305 This function generates for example: |
306 |
306 |
307 @{ML_response_fake [display,gray] |
307 @{ML_response_fake [display,gray] |
308 "writeln (string_of_term @{context} (term_tree 2))" |
308 "pwriteln (pretty_term @{context} (term_tree 2))" |
309 "(1 + 2) + (3 + 4)"} |
309 "(1 + 2) + (3 + 4)"} |
310 |
310 |
311 The next function constructs a goal of the form @{text "P \<dots>"} with a term |
311 The next function constructs a goal of the form @{text "P \<dots>"} with a term |
312 produced by @{ML term_tree} filled in. |
312 produced by @{ML term_tree} filled in. |
313 *} |
313 *} |