src/HOL/Auth/KerberosIV.ML

 (*The Oops1 case is unusual: must simplify Authkey \\<notin> analz (spies (ev#evs))
   rather than weakening it to Authkey \\<notin> analz (spies evs), for we then
   conclude AuthKey \\<noteq> AuthKeya.*)
 by (Clarify_tac 9);
 by analz_sees_tac;
-by (rotate_tac ~1 11);
 by (ALLGOALS 
     (asm_full_simp_tac 
      (simpset() addsimps [less_SucI, new_keys_not_analzd,
 			  Says_Kas_message_form, Says_Tgs_message_form,
 			  analz_insert_eq, not_parts_not_analz, 

 (*K5.  Not clear how this step could be integrated with the main
        simplification step.*)
 by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1);
 by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1);
 by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1);
-by (rotate_tac ~1 1);
 by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1);
 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
                         addIs  [less_SucI]) 1);
 qed_spec_mp "Confidentiality_lemma";