src/HOL/Auth/Yahalom2.ML
changeset 5932 737559a43e71
parent 5492 d9fc3457554e
child 6335 7e4bffaa2a3e
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 18 15:10:46 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Nov 18 16:24:33 1998 +0100
     1.3 @@ -196,8 +196,9 @@
     1.4  	        addsimps [analz_insert_eq, analz_insert_freshK])));
     1.5  (*Oops*)
     1.6  by (blast_tac (claset() addDs [unique_session_keys]) 3);
     1.7 -(*YM3*)
     1.8 -by (blast_tac (claset() delrules [impCE]) 2);
     1.9 +(*YM3: delete a useless induction hypothesis*)
    1.10 +by (thin_tac "?P-->?Q" 2);
    1.11 +by (Blast_tac 2);
    1.12  (*Fake*) 
    1.13  by (spy_analz_tac 1);
    1.14  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.15 @@ -350,10 +351,11 @@
    1.16  (*Fake*)
    1.17  by (Blast_tac 1);
    1.18  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
    1.19 -by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
    1.20 +by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
    1.21  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
    1.22  by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
    1.23 -(*yes: apply unicity of session keys*)
    1.24 +(*yes: delete a useless induction hypothesis; apply unicity of session keys*)
    1.25 +by (thin_tac "?P-->?Q" 1);
    1.26  by (not_bad_tac "Aa" 1);
    1.27  by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
    1.28  			addDs  [unique_session_keys]) 1);