src/HOL/TLA/Memory/MemoryImplementation.thy
changeset 27117 97e9dae57284
parent 27100 889613625e2b
child 27208 5fe899199f85
     1.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Jun 10 16:43:07 2008 +0200
     1.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Jun 10 16:43:14 2008 +0200
     1.3 @@ -763,12 +763,11 @@
     1.4  *)
     1.5  ML {*
     1.6  fun split_idle_tac ss simps i =
     1.7 -    EVERY [TRY (rtac @{thm actionI} i),
     1.8 -           DatatypePackage.case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
     1.9 -           rewrite_goals_tac @{thms action_rews},
    1.10 -           forward_tac [temp_use @{thm Step1_4_7}] i,
    1.11 -           asm_full_simp_tac (ss addsimps simps) i
    1.12 -          ]
    1.13 +  TRY (rtac @{thm actionI} i) THEN
    1.14 +  case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
    1.15 +  rewrite_goals_tac @{thms action_rews} THEN
    1.16 +  forward_tac [temp_use @{thm Step1_4_7}] i THEN
    1.17 +  asm_full_simp_tac (ss addsimps simps) i
    1.18  *}
    1.19  (* ----------------------------------------------------------------------
    1.20     Combine steps 1.2 and 1.4 to prove that the implementation satisfies