proper method_setup;

--- a/src/HOL/TLA/Inc/Inc.thy	Thu May 12 21:14:03 2011 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy	Thu May 12 22:07:30 2011 +0200
@@ -112,7 +112,7 @@
   by (auto simp: PsiInv_defs)
 
 lemma PsiInv: "|- Psi --> []PsiInv"
-  apply (tactic {* inv_tac (@{clasimpset} addsimps2 [@{thm Psi_def}]) 1 *})
+  apply (invariant simp: Psi_def)
    apply (force simp: PsiInv_Init [try_rewrite] Init_def)
   apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
     PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
@@ -125,7 +125,7 @@
 *)
 
 lemma "|- Psi --> []PsiInv"
-  by (tactic {* auto_inv_tac (@{simpset} addsimps (@{thms PsiInv_defs} @ @{thms Psi_defs})) 1 *})
+  by (auto_invariant simp: PsiInv_defs Psi_defs)
 
 
 (**** Step simulation ****)

--- a/src/HOL/TLA/Memory/Memory.thy	Thu May 12 21:14:03 2011 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy	Thu May 12 22:07:30 2011 +0200
@@ -147,8 +147,7 @@
 
 (* The memory spec implies the memory invariant *)
 lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
-  by (tactic {* auto_inv_tac
-    (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
+  by (auto_invariant simp: RM_temp_defs RM_action_defs)
 
 (* The invariant is trivial for non-locations *)
 lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"

--- a/src/HOL/TLA/TLA.thy	Thu May 12 21:14:03 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Thu May 12 22:07:30 2011 +0200
@@ -607,6 +607,16 @@
        (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
 *}
 
+method_setup invariant = {*
+  Method.sections Clasimp.clasimp_modifiers
+    >> (K (SIMPLE_METHOD' o inv_tac o clasimpset_of))
+*} ""
+
+method_setup auto_invariant = {*
+  Method.sections Clasimp.clasimp_modifiers
+    >> (K (SIMPLE_METHOD' o auto_inv_tac o simpset_of))
+*} ""
+
 lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
   apply (unfold dmd_def)
   apply (clarsimp dest!: BoxPrime [temp_use])