# HG changeset patch
# User wenzelm
# Date 1305288287 -7200
# Node ID 15ec9b3c14cc7c2e37dd89bc36ed52b2d5f908e8
# Parent  a2dca9a3d0dae8995398b127217105f8f3781f0e
proper method_setup "enabled";

diff -r a2dca9a3d0da -r 15ec9b3c14cc src/HOL/TLA/Action.thy
--- 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
 
diff -r a2dca9a3d0da -r 15ec9b3c14cc src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Fri May 13 13:45:20 2011 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy	Fri May 13 14:04:47 2011 +0200
@@ -161,7 +161,7 @@
 lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = gamma1 in enabled_mono)
-   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+   apply (enabled Inc_base)
   apply (force simp: gamma1_def)
   apply (force simp: angle_def gamma1_def N1_def)
   done
@@ -183,7 +183,7 @@
 lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = gamma2 in enabled_mono)
-  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+  apply (enabled Inc_base)
    apply (force simp: gamma2_def)
   apply (force simp: angle_def gamma2_def N2_def)
   done
@@ -202,7 +202,7 @@
 lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = beta2 in enabled_mono)
-   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+   apply (enabled Inc_base)
    apply (force simp: beta2_def)
   apply (force simp: angle_def beta2_def N2_def)
   done
@@ -244,7 +244,7 @@
   "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = alpha1 in enabled_mono)
-  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+  apply (enabled Inc_base)
    apply (force simp: alpha1_def PsiInv_defs)
   apply (force simp: angle_def alpha1_def N1_def)
   done
@@ -285,7 +285,7 @@
 lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = beta1 in enabled_mono)
-   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
+   apply (enabled Inc_base)
    apply (force simp: beta1_def)
   apply (force simp: angle_def beta1_def N1_def)
   done