equal
deleted
inserted
replaced
275 EVERY' [ |
275 EVERY' [ |
276 Seq_induct_tac ctxt sch |
276 Seq_induct_tac ctxt sch |
277 @{thms Filter_def Forall_def sforall_def mkex_def stutter_def}, |
277 @{thms Filter_def Forall_def sforall_def mkex_def stutter_def}, |
278 asm_full_simp_tac ctxt, |
278 asm_full_simp_tac ctxt, |
279 SELECT_GOAL |
279 SELECT_GOAL |
280 (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})), |
280 (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) \<^theory_context>\<open>Fun\<close>)), |
281 Seq_case_simp_tac ctxt exA, |
281 Seq_case_simp_tac ctxt exA, |
282 Seq_case_simp_tac ctxt exB, |
282 Seq_case_simp_tac ctxt exB, |
283 asm_full_simp_tac ctxt, |
283 asm_full_simp_tac ctxt, |
284 Seq_case_simp_tac ctxt exA, |
284 Seq_case_simp_tac ctxt exA, |
285 asm_full_simp_tac ctxt, |
285 asm_full_simp_tac ctxt, |