--- a/src/HOL/SET_Protocol/Public_SET.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy Wed Aug 10 09:33:54 2016 +0200
@@ -300,7 +300,7 @@
text\<open>Spy knows all public keys\<close>
lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy 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
declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
@@ -324,7 +324,7 @@
lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
-apply (simp_all add: used_Cons split add: event.split, safe)
+apply (simp_all add: used_Cons split: event.split, safe)
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done