equal
deleted
inserted
replaced
73 will print out @{text [quotes] "any string"} inside the response buffer |
73 will print out @{text [quotes] "any string"} inside the response buffer |
74 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
74 of Isabelle. This function expects a string as argument. If you develop under PolyML, |
75 then there is a convenient, though again ``quick-and-dirty'', method for |
75 then there is a convenient, though again ``quick-and-dirty'', method for |
76 converting values into strings, for example: |
76 converting values into strings, for example: |
77 |
77 |
78 @{ML_response_fake [display] "warning (makestring 1)" "1"} |
78 @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} |
79 |
79 |
80 However this only works if the type of what is converted is monomorphic and is not |
80 However this only works if the type of what is converted is monomorphic and is not |
81 a function. |
81 a function. |
82 |
82 |
83 The function @{ML "warning"} should only be used for testing purposes, because any |
83 The function @{ML "warning"} should only be used for testing purposes, because any |
155 |
155 |
156 @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
156 @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
157 @{ML_response_fake [display] "@{simpset}" "\<dots>"} |
157 @{ML_response_fake [display] "@{simpset}" "\<dots>"} |
158 |
158 |
159 (FIXME: what does a simpset look like? It seems to be the same problem |
159 (FIXME: what does a simpset look like? It seems to be the same problem |
160 like tokens.) |
160 as with tokens.) |
161 |
161 |
162 While antiquotations nowadays have many applications, they were originally introduced to |
162 While antiquotations nowadays have many applications, they were originally introduced to |
163 avoid explicit bindings for theorems such as |
163 avoid explicit bindings for theorems such as |
164 *} |
164 *} |
165 |
165 |