--- 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