src/HOL/Auth/Yahalom2.thy

     "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk>
      \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
 apply (erule rev_mp)
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy, simp_all)
-subgoal \<comment>\<open>Fake\<close> by (force dest!: keysFor_parts_insert)
-subgoal \<comment>\<open>YM3 \<close>by blast
-subgoal \<comment>\<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj])
+subgoal \<comment> \<open>Fake\<close> by (force dest!: keysFor_parts_insert)
+subgoal \<comment> \<open>YM3\<close>by blast
+subgoal \<comment> \<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj])
 done
 
 
 text\<open>Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.\<close>

           B \<notin> bad -->
           (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy)
 apply (analz_mono_contra, simp_all)
-  subgoal \<comment>\<open>Fake\<close> by blast
-  subgoal \<comment>\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
+  subgoal \<comment> \<open>Fake\<close> by blast
+  subgoal \<comment> \<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
     by (force dest!: Crypt_imp_keysFor)
-  subgoal \<comment>\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
+  subgoal \<comment> \<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
              otherwise by unicity of session keys\<close>
     by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
 done