src/Doc/Tutorial/Protocol/Event.thy

--- a/src/Doc/Tutorial/Protocol/Event.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -125,13 +125,13 @@
 lemma Says_imp_knows_Spy [rule_format]:
      "Says A B X \<in> set evs --> X \<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 done
 
 lemma Notes_imp_knows_Spy [rule_format]:
      "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 done
 
 
@@ -174,14 +174,14 @@
 text{*Agents know what they say*}
 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 apply blast
 done
 
 text{*Agents know what they note*}
 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 apply blast
 done
 
@@ -189,7 +189,7 @@
 lemma Gets_imp_knows_agents [rule_format]:
      "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 done
 
 
@@ -200,7 +200,7 @@
   Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
 apply (erule rev_mp)
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 apply blast
 done
 
@@ -211,7 +211,7 @@
   Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
 apply (erule rev_mp)
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
 apply blast
 done
 
@@ -224,7 +224,7 @@
 
 lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
 apply (induct_tac "evs")
-apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
+apply (simp_all add: parts_insert_knows_A split: event.split, blast)
 done
 
 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"