src/HOL/SET_Protocol/Cardholder_Registration.thy

   DK isn't a private encryption key may be an artifact of the particular
   definition of KeyCryptKey.\<close>
 lemma K_fresh_not_KeyCryptKey:
      "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
 apply (induct evs)
-apply (auto simp add: parts_insert2 split add: event.split)
+apply (auto simp add: parts_insert2 split: event.split)
 done
 
 
 text\<open>This holds because if (priEK (CA i)) appears in any traffic then it must
   be known to the Spy, by @{term Spy_see_private_Key}\<close>

 by (erule set_cr.induct, analz_mono_contra, auto)
 
 text\<open>Lemma for message 5: pubSK C is never used to encrypt Keys.\<close>
 lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
 apply (induct_tac "evs")
-apply (auto simp add: parts_insert2 split add: event.split)
+apply (auto simp add: parts_insert2 split: event.split)
 done
 
 text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
   or else cardSK hasn't been used to encrypt K.  Previously we treated
   message 5 in the same way, but the current model assumes that rule

   or else cardSK hasn't been used to encrypt K.\<close>
 
 text\<open>Lemma for message 5: pubSK C is never used to encrypt Nonces.\<close>
 lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
 apply (induct_tac "evs")
-apply (auto simp add: parts_insert2 split add: event.split)
+apply (auto simp add: parts_insert2 split: event.split)
 done
 
 text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
   or else cardSK hasn't been used to encrypt K.\<close>
 lemma msg6_KeyCryptNonce_disj: