equal
deleted
inserted
replaced
168 |
168 |
169 text {* |
169 text {* |
170 This function generates for example: |
170 This function generates for example: |
171 |
171 |
172 @{ML_response_fake [display,gray] |
172 @{ML_response_fake [display,gray] |
173 "warning (Syntax.string_of_term @{context} (term_tree 2))" |
173 "writeln (Syntax.string_of_term @{context} (term_tree 2))" |
174 "(1 + 2) + (3 + 4)"} |
174 "(1 + 2) + (3 + 4)"} |
175 |
175 |
176 The next function constructs a goal of the form @{text "P \<dots>"} with a term |
176 The next function constructs a goal of the form @{text "P \<dots>"} with a term |
177 produced by @{ML term_tree} filled in. |
177 produced by @{ML term_tree} filled in. |
178 *} |
178 *} |