equal
deleted
inserted
replaced
155 val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset} |
155 val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset} |
156 in |
156 in |
157 map #name (Net.entries rules) |
157 map #name (Net.entries rules) |
158 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
158 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"} |
159 |
159 |
160 In the second example, the function @{ML rep_ss in MetaSimplifier} returns a record |
160 The second example extracts the theorem names that are stored in a simpset. |
161 containing information about the simpset. The rules of a simpset are stored in a |
161 For this the function @{ML rep_ss in MetaSimplifier} returns a record |
162 discrimination net (a datastructure for fast indexing). From this net we can extract |
162 containing information about the simpset. The rules of a simpset are stored |
163 the entries using the function @{ML Net.entries}. |
163 in a discrimination net (a datastructure for fast indexing). From this net |
|
164 we can extract the entries using the function @{ML Net.entries}. |
164 |
165 |
165 While antiquotations have many applications, they were originally introduced to |
166 While antiquotations have many applications, they were originally introduced to |
166 avoid explicit bindings for theorems such as |
167 avoid explicit bindings for theorems such as |
167 *} |
168 *} |
168 |
169 |
183 |
184 |
184 text {* |
185 text {* |
185 One way to construct terms of Isabelle on the ML-level is by using the antiquotation |
186 One way to construct terms of Isabelle on the ML-level is by using the antiquotation |
186 \mbox{@{text "@{term \<dots>}"}}. For example |
187 \mbox{@{text "@{term \<dots>}"}}. For example |
187 |
188 |
188 @{ML_response [display] "@{term \"(a::nat) + b = c\"}" |
189 @{ML_response [display] |
189 "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
190 "@{term \"(a::nat) + b = c\"}" |
|
191 "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
190 |
192 |
191 This will show the term @{term "(a::nat) + b = c"}, but printed using the internal |
193 This will show the term @{term "(a::nat) + b = c"}, but printed using the internal |
192 representation of this term. This internal representation corresponds to the |
194 representation of this term. This internal representation corresponds to the |
193 datatype @{ML_type "term"}. |
195 datatype @{ML_type "term"}. |
194 |
196 |