equal
deleted
inserted
replaced
692 by (etac otway.induct 1); |
692 by (etac otway.induct 1); |
693 by analz_Fake_tac; |
693 by analz_Fake_tac; |
694 (*spy_analz_tac just does not work here: it is an entirely different proof!*) |
694 (*spy_analz_tac just does not work here: it is an entirely different proof!*) |
695 by (ALLGOALS |
695 by (ALLGOALS |
696 (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib, |
696 (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib, |
697 imp_conj_distrib, parts_insert_sees, |
697 imp_conjR, parts_insert_sees, |
698 parts_insert2]))); |
698 parts_insert2]))); |
699 by (REPEAT_FIRST (etac exE)); |
699 by (REPEAT_FIRST (etac exE)); |
700 (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **) |
700 (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **) |
701 by (expand_case_tac "K = ?y" 4); |
701 by (expand_case_tac "K = ?y" 4); |
702 by (REPEAT (ares_tac [exI] 5)); |
702 by (REPEAT (ares_tac [exI] 5)); |