--- a/src/HOL/TLA/Action.thy Fri May 13 13:45:20 2011 +0200
+++ b/src/HOL/TLA/Action.thy Fri May 13 14:04:47 2011 +0200
@@ -277,16 +277,20 @@
The following tactic combines these steps except the final one.
*)
-fun enabled_tac (cs, ss) base_vars =
- clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);
+fun enabled_tac ctxt base_vars =
+ clarsimp_tac (claset_of ctxt addSIs [base_vars RS @{thm base_enabled}], simpset_of ctxt);
*}
+method_setup enabled = {*
+ Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
+*} ""
+
(* Example *)
lemma
assumes "basevars (x,y,z)"
shows "|- x --> Enabled ($x & (y$ = #False))"
- apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})
+ apply (enabled assms)
apply auto
done