equal
deleted
inserted
replaced
237 The tactic will use the following helper function for instantiating universal |
237 The tactic will use the following helper function for instantiating universal |
238 quantifiers. |
238 quantifiers. |
239 *} |
239 *} |
240 |
240 |
241 ML{*fun inst_spec ctrm = |
241 ML{*fun inst_spec ctrm = |
242 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*} |
242 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] |
243 |
243 @{thm spec}*} |
244 text {* |
244 |
245 This helper function instantiates the @{text "?x"} in the theorem |
245 text {* |
246 @{thm spec} with a given @{ML_type cterm}. We call this helper function |
246 This helper function uses the function @{ML_ind instantiate' in Drule} |
247 in the following tactic.\label{fun:instspectac}. |
247 and instantiates the @{text "?x"} in the theorem @{thm spec} with a given |
|
248 @{ML_type cterm}. We call this helper function in the following |
|
249 tactic.\label{fun:instspectac}. |
248 *} |
250 *} |
249 |
251 |
250 ML{*fun inst_spec_tac ctrms = |
252 ML{*fun inst_spec_tac ctrms = |
251 EVERY' (map (dtac o inst_spec) ctrms)*} |
253 EVERY' (map (dtac o inst_spec) ctrms)*} |
252 |
254 |