equal
deleted
inserted
replaced
394 apply (subst fun_upd_twist) |
394 apply (subst fun_upd_twist) |
395 apply (erule not_sym) |
395 apply (erule not_sym) |
396 apply (rename_tac "ba") |
396 apply (rename_tac "ba") |
397 apply (drule_tac x = "ba" in spec) |
397 apply (drule_tac x = "ba" in spec) |
398 apply clarify |
398 apply clarify |
399 apply (tactic "smp_tac @{context} 2 1") |
399 apply (tactic "smp_tac \<^context> 2 1") |
400 apply (erule (1) notE impE) |
400 apply (erule (1) notE impE) |
401 apply (case_tac "aa = b") |
401 apply (case_tac "aa = b") |
402 apply fast+ |
402 apply fast+ |
403 done |
403 done |
404 declare fun_upd_apply [simp] |
404 declare fun_upd_apply [simp] |