# HG changeset patch
# User wenzelm
# Date 1305231076 -7200
# Node ID 3ebce8d71a059570aec05ff2c652e6bd1befabcc
# Parent  053b4b487085cf7c02836a7084ddeffff08f67a4
eliminated obsolete MI_css -- use current context directly;

diff -r 053b4b487085 -r 3ebce8d71a05 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu May 12 22:07:30 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu May 12 22:11:16 2011 +0200
@@ -218,8 +218,6 @@
 
 declare if_weak_cong [cong del]
 
-ML {* val MI_css = (@{claset}, @{simpset}) *}
-
 (* A more aggressive variant that tries to solve subgoals by assumption
    or contradiction during the simplification.
    THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
@@ -229,7 +227,7 @@
 ML {*
 val MI_fast_css =
   let
-    val (cs,ss) = MI_css
+    val (cs,ss) = @{clasimpset}
   in
     (cs addSEs [temp_use @{thm squareE}],
       ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
@@ -1203,7 +1201,7 @@
 lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p)
          & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
          --> []ImpInv rmhist p"
-  apply (tactic "inv_tac MI_css 1")
+  apply invariant
    apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
      dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
      S3_successors [temp_use] S4_successors [temp_use] S5_successors [temp_use]