changeset 239 | b63c72776f03 |
parent 225 | 7859fc59249a |
child 272 | 2ff4867c00cf |
--- a/ProgTutorial/Solutions.thy Mon Apr 13 08:30:48 2009 +0000 +++ b/ProgTutorial/Solutions.thy Wed Apr 15 13:11:08 2009 +0000 @@ -170,7 +170,7 @@ This function generates for example: @{ML_response_fake [display,gray] - "warning (Syntax.string_of_term @{context} (term_tree 2))" + "writeln (Syntax.string_of_term @{context} (term_tree 2))" "(1 + 2) + (3 + 4)"} The next function constructs a goal of the form @{text "P \<dots>"} with a term