src/HOL/Auth/Yahalom.ML

 \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by analz_Fake_tac;
 by (ALLGOALS  (*22 seconds*)
     (asm_simp_tac 
-     (!simpset addsimps ([not_parts_not_analz,
-                          analz_image_newK,
+     (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
                           insert_Key_singleton, insert_Key_image]
                          @ pushes)
                setloop split_tac [expand_if])));
 (*Base*)
 by (fast_tac (!claset addss (!simpset)) 1);

 by (grind_tac 2);
 by (fast_tac (!claset delrules [bexI] 
                       addDs [unique_session_keys]
                       addss (!simpset)) 2);
 (*YM4*)
-(** LEVEL 11 **)
+(** LEVEL 10 **)
 by (rtac (impI RS allI) 1);
 by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
 by (asm_simp_tac (!simpset addsimps [analz_image_newK]
                            setloop split_tac [expand_if]) 1);
-(** LEVEL 15 **)
+(** LEVEL 14 **)
 by (grind_tac 1);
 by (REPEAT (dtac not_analz_insert 1));
 by (lost_tac "A" 1);
 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
     THEN REPEAT (assume_tac 1));