diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Public.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -309,7 +309,7 @@
 text\<open>All public keys are visible\<close>
 lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
 apply (induct_tac "evs")
-apply (auto simp add: imageI knows_Cons split add: event.split)
+apply (auto simp add: imageI knows_Cons split: event.split)
 done
 
 lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
@@ -319,14 +319,14 @@
 lemma Spy_spies_bad_privateKey [intro!]:
      "A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
 apply (induct_tac "evs")
-apply (auto simp add: imageI knows_Cons split add: event.split)
+apply (auto simp add: imageI knows_Cons split: event.split)
 done
 
 text\<open>Spy sees long-term shared keys of bad agents!\<close>
 lemma Spy_spies_bad_shrK [intro!]:
      "A \<in> bad ==> Key (shrK A) \<in> spies evs"
 apply (induct_tac "evs")
-apply (simp_all add: imageI knows_Cons split add: event.split)
+apply (simp_all add: imageI knows_Cons split: event.split)
 done
 
 lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
@@ -361,7 +361,7 @@
 lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
 apply (induct_tac "evs")
 apply (rule_tac x = 0 in exI)
-apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
 apply safe
 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
 done