equal
deleted
inserted
replaced
762 steps of the implementation, and try to solve the idling case by simplification |
762 steps of the implementation, and try to solve the idling case by simplification |
763 *) |
763 *) |
764 ML {* |
764 ML {* |
765 fun split_idle_tac ss simps i = |
765 fun split_idle_tac ss simps i = |
766 EVERY [TRY (rtac @{thm actionI} i), |
766 EVERY [TRY (rtac @{thm actionI} i), |
767 case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i, |
767 DatatypePackage.case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i, |
768 rewrite_goals_tac @{thms action_rews}, |
768 rewrite_goals_tac @{thms action_rews}, |
769 forward_tac [temp_use @{thm Step1_4_7}] i, |
769 forward_tac [temp_use @{thm Step1_4_7}] i, |
770 asm_full_simp_tac (ss addsimps simps) i |
770 asm_full_simp_tac (ss addsimps simps) i |
771 ] |
771 ] |
772 *} |
772 *} |