src/HOL/TLA/Memory/MemoryImplementation.thy
changeset 45133 2214ba5bdfff
parent 43596 78211f66cf8d
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Oct 12 22:21:38 2011 +0200
     1.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Oct 12 22:48:23 2011 +0200
     1.3 @@ -794,7 +794,7 @@
     1.4  fun split_idle_tac ctxt =
     1.5    SELECT_GOAL
     1.6     (TRY (rtac @{thm actionI} 1) THEN
     1.7 -    InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
     1.8 +    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" 1 THEN
     1.9      rewrite_goals_tac @{thms action_rews} THEN
    1.10      forward_tac [temp_use @{thm Step1_4_7}] 1 THEN
    1.11      asm_full_simp_tac (simpset_of ctxt) 1);