148 replaced with the value representing the theory name. |
148 replaced with the value representing the theory name. |
149 |
149 |
150 In a similar way you can use antiquotations to refer to theorems or simpsets: |
150 In a similar way you can use antiquotations to refer to theorems or simpsets: |
151 |
151 |
152 @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
152 @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"} |
153 @{ML_response_fake [display] "@{simpset}" "\<dots>"} |
153 @{ML_response_fake [display] |
154 |
154 "let |
155 (FIXME: what does a simpset look like? It seems to be the same problem |
155 val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset} |
156 as with tokens.) |
156 in |
157 |
157 map #name (Net.entries rules) |
158 While antiquotations have many applications, they were originally introduced to |
158 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
|
159 |
|
160 In the second example, the function @{ML rep_ss in MetaSimplifier} returns a record |
|
161 containing information about the simpset. The rules of a simpset are stored in a |
|
162 discrimination net (a datastructure for fast indexing). From this net we can extract |
|
163 the entries using the function @{ML Net.entries}. |
|
164 |
|
165 While antiquotations have many applications, they were originally introduced to |
159 avoid explicit bindings for theorems such as |
166 avoid explicit bindings for theorems such as |
160 *} |
167 *} |
161 |
168 |
162 ML{*val allI = thm "allI" *} |
169 ML{*val allI = thm "allI" *} |
163 |
170 |