equal
deleted
inserted
replaced
276 - Solve for the unknowns using standard HOL reasoning. |
276 - Solve for the unknowns using standard HOL reasoning. |
277 The following tactic combines these steps except the final one. |
277 The following tactic combines these steps except the final one. |
278 *) |
278 *) |
279 |
279 |
280 fun enabled_tac ctxt base_vars = |
280 fun enabled_tac ctxt base_vars = |
281 clarsimp_tac (claset_of ctxt addSIs [base_vars RS @{thm base_enabled}], simpset_of ctxt); |
281 clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]); |
282 *} |
282 *} |
283 |
283 |
284 method_setup enabled = {* |
284 method_setup enabled = {* |
285 Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th)) |
285 Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th)) |
286 *} "" |
286 *} "" |