changeset 440 | a0b280dd4bc7 |
parent 426 | d94755882e36 |
child 441 | 520127b708e6 |
--- a/ProgTutorial/Solutions.thy Mon Jul 19 15:44:13 2010 +0100 +++ b/ProgTutorial/Solutions.thy Tue Jul 20 13:34:44 2010 +0100 @@ -305,7 +305,7 @@ This function generates for example: @{ML_response_fake [display,gray] - "writeln (string_of_term @{context} (term_tree 2))" + "pwriteln (pretty_term @{context} (term_tree 2))" "(1 + 2) + (3 + 4)"} The next function constructs a goal of the form @{text "P \<dots>"} with a term