# 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]