equal
deleted
inserted
replaced
806 \ ExpirAuth Tk evs"; |
806 \ ExpirAuth Tk evs"; |
807 by (etac kerberos.induct 1); |
807 by (etac kerberos.induct 1); |
808 by analz_sees_tac; |
808 by analz_sees_tac; |
809 by (ALLGOALS |
809 by (ALLGOALS |
810 (asm_simp_tac |
810 (asm_simp_tac |
811 (simpset() addsimps ([Says_Kas_message_form, |
811 (simpset() addsimps ([Says_Kas_message_form, less_SucI, |
812 analz_insert_eq, not_parts_not_analz, |
812 analz_insert_eq, not_parts_not_analz, |
813 analz_insert_freshK1] @ pushes)))); |
813 analz_insert_freshK1] @ pushes)))); |
814 (*Fake*) |
814 (*Fake*) |
815 by (spy_analz_tac 1); |
815 by (spy_analz_tac 1); |
816 (*K2*) |
816 (*K2*) |
866 by (Clarify_tac 9); |
866 by (Clarify_tac 9); |
867 by analz_sees_tac; |
867 by analz_sees_tac; |
868 by (rotate_tac ~1 11); |
868 by (rotate_tac ~1 11); |
869 by (ALLGOALS |
869 by (ALLGOALS |
870 (asm_full_simp_tac |
870 (asm_full_simp_tac |
871 (simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form, |
871 (simpset() addsimps [less_SucI, |
872 analz_insert_eq, not_parts_not_analz, |
872 Says_Kas_message_form, Says_Tgs_message_form, |
873 analz_insert_freshK1, analz_insert_freshK2] @ pushes)))); |
873 analz_insert_eq, not_parts_not_analz, |
|
874 analz_insert_freshK1, analz_insert_freshK2] |
|
875 @ pushes))); |
874 (*Fake*) |
876 (*Fake*) |
875 by (spy_analz_tac 1); |
877 by (spy_analz_tac 1); |
876 (*K2*) |
878 (*K2*) |
877 by (blast_tac (claset() addSEs spies_partsEs |
879 by (blast_tac (claset() addSEs spies_partsEs |
878 addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1); |
880 addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1); |