--- a/CookBook/FirstSteps.thy Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/FirstSteps.thy Sat Jan 03 20:44:54 2009 +0000
@@ -75,7 +75,7 @@
then there is a convenient, though again ``quick-and-dirty'', method for
converting values into strings, for example:
- @{ML_response_fake [display] "warning (makestring 1)" "1"}
+ @{ML_response_fake [display] "warning (makestring 1)" "\"1\""}
However this only works if the type of what is converted is monomorphic and is not
a function.
@@ -157,7 +157,7 @@
@{ML_response_fake [display] "@{simpset}" "\<dots>"}
(FIXME: what does a simpset look like? It seems to be the same problem
- like tokens.)
+ as with tokens.)
While antiquotations nowadays have many applications, they were originally introduced to
avoid explicit bindings for theorems such as