# HG changeset patch
# User nipkow
# Date 1470814434 -7200
# Node ID f9f3006a5579b2b686eaa1b2f0f2979c13aacad8
# Parent  437bd400d8084c8c1c229c001c0a8616c5211b42
"split add" -> "split"

diff -r 437bd400d808 -r f9f3006a5579 src/Doc/Tutorial/Inductive/AB.thy
--- a/src/Doc/Tutorial/Inductive/AB.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Inductive/AB.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -264,7 +264,7 @@
 *}
 
   apply(force simp add: min_less_iff_disj)
- apply(force split add: nat_diff_split)
+ apply(force split: nat_diff_split)
 
 txt{*
 The case @{prop"w = b#v"} is proved analogously:
@@ -278,7 +278,7 @@
 apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
 apply(rule S_A_B.intros)
  apply(force simp add: min_less_iff_disj)
-by(force simp add: min_less_iff_disj split add: nat_diff_split)
+by(force simp add: min_less_iff_disj split: nat_diff_split)
 
 text{*
 We conclude this section with a comparison of our proof with 
diff -r 437bd400d808 -r f9f3006a5579 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"
diff -r 437bd400d808 -r f9f3006a5579 src/Doc/Tutorial/Protocol/Public.thy
--- a/src/Doc/Tutorial/Protocol/Public.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Protocol/Public.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -130,7 +130,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
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Event.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -124,13 +124,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
 
 
@@ -164,14 +164,14 @@
 text\<open>Agents know what they say\<close>
 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\<open>Agents know what they note\<close>
 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
 
@@ -179,7 +179,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
 
 
@@ -190,7 +190,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
 
@@ -201,7 +201,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
 
@@ -214,7 +214,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"
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
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Shared.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -78,7 +78,7 @@
 (*Spy sees shared keys of agents!*)
 lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
 done
 
 (*For case analysis on whether or not an agent is compromised*)
@@ -123,7 +123,7 @@
 lemma Nonce_supply_lemma: "\<exists>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 (metis le_sup_iff msg_Nonce_supply)
 done
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Auth/Smartcard/EventSC.thy
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -196,13 +196,13 @@
 lemma Says_imp_knows_Spy [rule_format]:
      "Says A B X \<in> set evs \<longrightarrow> 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 \<longrightarrow> A\<in> bad \<longrightarrow> 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
 
 (*Nothing can be stated on a Gets event*)
@@ -210,13 +210,13 @@
 lemma Inputs_imp_knows_Spy_secureM [rule_format (no_asm)]: 
      "Inputs Spy C X \<in> set evs \<longrightarrow> secureM \<longrightarrow> 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 Inputs_imp_knows_Spy_insecureM [rule_format (no_asm)]:
      "Inputs A C X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> 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
 
 (*Nothing can be stated on a C_Gets event*)
@@ -224,13 +224,13 @@
 lemma Outpts_imp_knows_Spy_secureM [rule_format (no_asm)]: 
      "Outpts C Spy X \<in> set evs \<longrightarrow> secureM \<longrightarrow> 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 Outpts_imp_knows_Spy_insecureM [rule_format (no_asm)]:
      "Outpts C A X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> 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
 
 (*Nothing can be stated on an A_Gets event*)
@@ -290,14 +290,14 @@
 text\<open>Agents know what they say\<close>
 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> 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\<open>Agents know what they note\<close>
 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> 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
 
@@ -305,14 +305,14 @@
 lemma Gets_imp_knows_agents [rule_format]:
      "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> 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
 
 (*Agents know what they input to their smart card*)
 lemma Inputs_imp_knows_agents [rule_format (no_asm)]: 
      "Inputs A (Card A) X \<in> set evs \<longrightarrow> 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
 
@@ -323,14 +323,14 @@
 lemma Outpts_imp_knows_agents_secureM [rule_format (no_asm)]: 
      "secureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> 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
 
 (*otherwise only the spy knows the outputs*)
 lemma Outpts_imp_knows_agents_insecureM [rule_format (no_asm)]: 
       "insecureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> 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
 
 (*end lemmas about agents' knowledge*)
@@ -346,7 +346,7 @@
 
 lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> 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
 
 simps_of_case used_Cons_simps[simp]: used_Cons
@@ -362,28 +362,28 @@
 lemma Says_parts_used [rule_format (no_asm)]: 
      "Says A B X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used 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
 
 lemma Notes_parts_used [rule_format (no_asm)]: 
      "Notes A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used 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
 
 lemma Outpts_parts_used [rule_format (no_asm)]: 
      "Outpts C A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used 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
 
 lemma Inputs_parts_used [rule_format (no_asm)]: 
      "Inputs A C X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used 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
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -137,7 +137,7 @@
 (*Spy knows the pins of bad agents!*)
 lemma Spy_knows_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
 done
 
 (*Spy knows the long-term keys of cloned cards!*)
@@ -147,24 +147,24 @@
                            Key (pin A)  \<in> knows Spy evs &  
                           (\<forall> B. Key (pairK(B,A)) \<in> knows Spy evs)"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
 done
 
 lemma Spy_knows_cloned1 [intro!]: "C \<in> cloned \<Longrightarrow> Key (crdK C) \<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
 done
 
 lemma Spy_knows_cloned2 [intro!]: "\<lbrakk> Card A \<in> cloned; Card B \<in> cloned \<rbrakk>  
    \<Longrightarrow> Nonce (Pairkey(A,B))\<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
 done
 
 (*Spy only knows pins of bad agents!*)
 lemma Spy_knows_Spy_bad [intro!]: "A\<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
 apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
 done
 
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -56,7 +56,7 @@
 
 lemma nyinitcls_init_lvars [simp]: 
   "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
-  by (induct s) (simp add: init_lvars_def2 split add: if_split)
+  by (induct s) (simp add: init_lvars_def2 split: if_split)
 
 lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
   unfolding nyinitcls_def by fast
@@ -74,7 +74,7 @@
 apply  (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
 apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
 apply   (auto dest!: not_initedD elim!: 
-              simp add: nyinitcls_def inited_def split add: if_split_asm)
+              simp add: nyinitcls_def inited_def split: if_split_asm)
 done
 
 lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
@@ -1072,7 +1072,7 @@
         apply (rule ax_derivs.NewA 
                [where ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty T) 
                               \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"])
-        apply  (simp add: init_comp_ty_def split add: if_split)
+        apply  (simp add: init_comp_ty_def split: if_split)
         apply  (rule conjI, clarsimp)
         apply   (rule MGFn_InitD [OF hyp, THEN conseq2])
         apply   (clarsimp intro: eval.Init)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/Conform.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -207,7 +207,7 @@
 apply (unfold lconf_def)
 apply safe
 apply (case_tac [3] "n")
-apply (force split add: sum.split)+
+apply (force split: sum.split)+
 done
 
 lemma lconf_ext_list [rule_format (no_asm)]: "
@@ -288,7 +288,7 @@
 apply (unfold wlconf_def)
 apply safe
 apply (case_tac [3] "n")
-apply (force split add: sum.split)+
+apply (force split: sum.split)+
 done
 
 lemma wlconf_ext_list [rule_format (no_asm)]: "
@@ -370,7 +370,7 @@
 apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
 defer
 apply (subst obj_ty_cong)
-apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
+apply (auto dest!: fields_table_SomeD split: sum.split_asm obj_tag.split_asm)
 done
 
 subsubsection "state conformance"
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/Decl.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -69,22 +69,22 @@
 proof
   fix x y z::acc_modi
   show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
-    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
+    by (auto simp add: le_acc_def less_acc_def split: acc_modi.split) 
   show "x \<le> x"                       \<comment> reflexivity
     by (auto simp add: le_acc_def)
   {
     assume "x \<le> y" "y \<le> z"           \<comment> transitivity 
     then show "x \<le> z"
-      by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
+      by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
   next
     assume "x \<le> y" "y \<le> x"           \<comment> antisymmetry
     moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
-      by (auto simp add: less_acc_def split add: acc_modi.split)
+      by (auto simp add: less_acc_def split: acc_modi.split)
     ultimately show "x = y" by (unfold le_acc_def) iprover
   next
     fix x y:: acc_modi
     show "x \<le> y \<or> y \<le> x"   
-      by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
+      by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
   }
 qed
   
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/Eval.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1166,12 +1166,12 @@
       [strip_tac @{context}, rotate_tac ~1, eresolve_tac @{context} @{thms eval_elim_cases}])\<close>)
 (* 31 subgoals *)
 prefer 28 (* Try *) 
-apply (simp (no_asm_use) only: split add: if_split_asm)
+apply (simp (no_asm_use) only: split: if_split_asm)
 (* 34 subgoals *)
 prefer 30 (* Init *)
 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+)
 prefer 26 (* While *)
-apply (simp (no_asm_use) only: split add: if_split_asm, blast)
+apply (simp (no_asm_use) only: split: if_split_asm, blast)
 (* 36 subgoals *)
 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
 done
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/State.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -97,7 +97,7 @@
 lemma obj_ty_widenD: 
  "G\<turnstile>obj_ty obj\<preceq>RefT t \<Longrightarrow> (\<exists>C. tag obj = CInst C) \<or> (\<exists>T k. tag obj = Arr T k)"
 apply (unfold obj_ty_def)
-apply (auto split add: obj_tag.split_asm)
+apply (auto split: obj_tag.split_asm)
 done
 
 definition
@@ -207,7 +207,7 @@
                  fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) nt 
                   = Some T))"
 apply (unfold var_tys_def arr_comps_def)
-apply (force split add: sum.split_asm sum.split obj_tag.split)
+apply (force split: sum.split_asm sum.split obj_tag.split)
 done
 
 
@@ -704,7 +704,7 @@
 
 lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)"
 apply (unfold inited_def)
-apply (auto split add: st.split)
+apply (auto split: st.split)
 done
 
 lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))"
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -213,7 +213,7 @@
 apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
  simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
             check_field_access_def check_method_access_def Let_def
- split del: if_split_asm split add: sum3.split)
+ split del: if_split_asm split: sum3.split)
 (* 6 subgoals *)
 apply force+
 done
@@ -632,7 +632,7 @@
 apply (case_tac "mode = IntVir")
 apply (drule conf_RefTD)
 apply (force intro!: conf_AddrI 
-            simp add: obj_class_def split add: obj_tag.split_asm)
+            simp add: obj_class_def split: obj_tag.split_asm)
 apply  clarsimp
 apply  safe
 apply    (erule (1) widen.subcls [THEN conf_widen])
@@ -655,7 +655,7 @@
 
 lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
     x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
-apply (auto split add: split_abrupt_if simp add: throw_def2)
+apply (auto split: split_abrupt_if simp add: throw_def2)
 apply (erule conforms_xconf)
 apply (frule conf_RefTD)
 apply (auto elim: widen.subcls [THEN conf_widen])
@@ -674,7 +674,7 @@
 "\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L);
   dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
 \<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
-apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
+apply (auto elim: eval_gext' conforms_xgext split: split_abrupt_if)
 done
 
 lemma FVar_lemma1: 
@@ -700,7 +700,7 @@
 apply  (erule fields_table_SomeI, simp (no_asm))
 apply clarsimp
 apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
-apply (auto dest!: widen_Array split add: obj_tag.split)
+apply (auto dest!: widen_Array split: obj_tag.split)
 apply (rule fields_table_SomeI)
 apply (auto elim!: fields_mono subcls_is_class2)
 done
@@ -829,7 +829,7 @@
    =
   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
 apply (unfold lconf_def)
-apply (auto split add: lname.splits)
+apply (auto split: lname.splits)
 done
 
 lemma wlconf_map_lname [simp]: 
@@ -837,7 +837,7 @@
    =
   (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
 apply (unfold wlconf_def)
-apply (auto split add: lname.splits)
+apply (auto split: lname.splits)
 done
 
 lemma lconf_map_ename [simp]:
@@ -845,7 +845,7 @@
    =
   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
 apply (unfold lconf_def)
-apply (auto split add: ename.splits)
+apply (auto split: ename.splits)
 done
 
 lemma wlconf_map_ename [simp]:
@@ -853,7 +853,7 @@
    =
   (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
 apply (unfold wlconf_def)
-apply (auto split add: ename.splits)
+apply (auto split: ename.splits)
 done
 
 
@@ -902,7 +902,7 @@
                               then None else Some (Class declC)))"
 apply (simp add: init_lvars_def2)
 apply (rule conforms_set_locals)
-apply  (simp (no_asm_simp) split add: if_split)
+apply  (simp (no_asm_simp) split: if_split)
 apply (drule  (4) DynT_conf)
 apply clarsimp
 (* apply intro *)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Binomial.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -317,7 +317,7 @@
 text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close>
 lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
   using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
-  by (auto split add: nat_diff_split)
+  by (auto split: nat_diff_split)
 
 
 subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Deriv.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1095,7 +1095,7 @@
     fix h :: real
     assume "0 < h" "h < s" "x - h \<in> S"
     with all [of "x - h"] show "f x < f (x-h)"
-    proof (simp add: abs_if pos_less_divide_eq dist_real_def split add: if_split_asm)
+    proof (simp add: abs_if pos_less_divide_eq dist_real_def split: if_split_asm)
       assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
       with l have "0 < (f (x-h) - f x) / h"
         by arith
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1405,7 +1405,7 @@
   apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
    prefer 2 apply (blast intro: finite_subset, atomize)
   apply (drule_tac x = "A - {x}" in spec)
-  apply (simp add: card_Diff_singleton_if split add: if_split_asm)
+  apply (simp add: card_Diff_singleton_if split: if_split_asm)
   apply (case_tac "card A", auto)
   done
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -155,14 +155,14 @@
 apply (rule impI)
 apply (erule conjE)+
 apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
-  split add: if_split)
+  split: if_split)
 txt \<open>detour 2\<close>
 apply (tactic "tac @{context} 1")
 apply (tactic "tac_ren @{context} 1")
 apply (rule impI)
 apply (erule conjE)+
 apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
-  Multiset.delm_nonempty_def split add: if_split)
+  Multiset.delm_nonempty_def split: if_split)
 apply (rule allI)
 apply (rule conjI)
 apply (rule impI)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/NTP/Lemmas.thy
--- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -25,7 +25,7 @@
 subsection \<open>Arithmetic\<close>
 
 lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
-  by (simp add: diff_Suc split add: nat.split)
+  by (simp add: diff_Suc split: nat.split)
 
 lemmas [simp] = hd_append set_lemmas
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/RefCorrectness.thy
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -189,7 +189,7 @@
   apply (auto simp add: mk_traceConc)
   apply (frule reachable.reachable_n)
   apply assumption
-  apply (auto simp add: move_subprop4 split add: if_split)
+  apply (auto simp add: move_subprop4 split: if_split)
   done
 
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/Seq.thy
--- a/src/HOL/HOLCF/IOA/Seq.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Seq.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
 
 theory Seq
-imports "../../HOLCF"
+imports "../HOLCF"
 begin
 
 default_sort pcpo
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/SimCorrectness.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -173,7 +173,7 @@
   apply (erule_tac x = "t" in allE)
   apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
   apply (simp add: move_subprop5_sim [unfolded Let_def]
-    move_subprop4_sim [unfolded Let_def] split add: if_split)
+    move_subprop4_sim [unfolded Let_def] split: if_split)
   done
 
 text \<open>Lemma 2: \<open>corresp_ex_sim\<close> is execution\<close>
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TL.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -128,7 +128,7 @@
   apply (erule_tac x = "s" in allE)
   apply (simp add: tsuffix_def suffix_refl)
   text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close>
-  apply (simp split add: if_split)
+  apply (simp split: if_split)
   apply auto
   apply (drule tsuffix_TL2)
   apply assumption+
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -140,7 +140,7 @@
               \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))"
   apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
   apply clarify
-  apply (simp split add: if_split)
+  apply (simp split: if_split)
   text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
   apply (pair ex)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/IOA/Solve.thy
--- a/src/HOL/IOA/Solve.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/IOA/Solve.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -86,7 +86,7 @@
   apply (simp cong del: if_weak_cong
     add: executions_def is_execution_fragment_def par_def starts_of_def
       trans_of_def filter_oseq_def
-    split add: option.split)
+    split: option.split)
   done
 
 
@@ -103,7 +103,7 @@
   apply (simp cong del: if_weak_cong
     add: executions_def is_execution_fragment_def par_def starts_of_def
     trans_of_def filter_oseq_def
-    split add: option.split)
+    split: option.split)
   done
 
 declare if_split [split del] if_weak_cong [cong del]
@@ -143,7 +143,7 @@
 (* delete auxiliary subgoal *)
   prefer 2
   apply force
-  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: if_split)
+  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split: if_split)
   apply (tactic \<open>
     REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
       asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1)\<close>)
@@ -157,7 +157,7 @@
   apply (simp (no_asm))
 (* execution is indeed an execution of C *)
   apply (simp add: executions_def is_execution_fragment_def par_def
-    starts_of_def trans_of_def rename_def split add: option.split)
+    starts_of_def trans_of_def rename_def split: option.split)
   apply force
   done
 
@@ -197,7 +197,7 @@
   apply assumption
   apply simp
 (* x is internal *)
-  apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
+  apply (simp (no_asm) cong add: conj_cong)
   apply (rule impI)
   apply (erule conjE)
   apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Int.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1190,7 +1190,7 @@
 apply (case_tac "k = f (Suc n)")
 apply force
 apply (erule impE)
- apply (simp add: abs_if split add: if_split_asm)
+ apply (simp add: abs_if split: if_split_asm)
 apply (blast intro: le_SucI)
 done
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Aug 10 09:33:54 2016 +0200
@@ -266,7 +266,7 @@
   by auto};
 
 val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
-  by (atomize (full)) (auto split add: abs_split)};
+  by (atomize (full)) (auto split: abs_split)};
 
 val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
   by (atomize (full)) (cases "x <= y", auto simp add: max_def)};
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Map.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -312,7 +312,7 @@
 apply (induct xs)
  apply simp
 apply (rule ext)
-apply (simp split add: option.split)
+apply (simp split: option.split)
 done
 
 lemma finite_range_map_of_map_add:
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -191,7 +191,7 @@
 lemma class_tprgD: 
 "class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
 apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
-apply (auto split add: if_split_asm simp add: map_of_Cons)
+apply (auto split: if_split_asm simp add: map_of_Cons)
 done
 
 lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R"
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -234,7 +234,7 @@
 apply( erule conjI)
 apply( clarsimp)
 apply( drule eval_no_xcpt)
-apply( simp split add: binop.split)
+apply( simp split: binop.split)
 
 \<comment> "12 LAcc"
 apply simp
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -146,7 +146,7 @@
 lemma wf_cdecl_supD: 
 "!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
 apply (unfold ws_cdecl_def)
-apply (auto split add: option.split_asm)
+apply (auto split: option.split_asm)
 done
 
 lemma subcls_asym: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> (D, C) \<notin> (subcls1 G)^+"
@@ -534,7 +534,7 @@
  apply (simp add: map_of_map)
  apply (clarify)
  apply (subst method_rec, assumption+)
- apply (simp add: map_add_def map_of_map split add: option.split)
+ apply (simp add: map_add_def map_of_map split: option.split)
 done
 
 
@@ -554,7 +554,7 @@
  apply (simp add: map_of_map)
  apply (clarify)
  apply (subst method_rec, assumption+)
- apply (simp add: map_add_def map_of_map split add: option.split)
+ apply (simp add: map_add_def map_of_map split: option.split)
 done
 
 lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -215,7 +215,7 @@
 apply (rule ty_expr_ty_exprs_wt_stmt.induct)
 apply auto
 apply (   erule typeof_empty_is_type)
-apply (  simp split add: if_split_asm)
+apply (  simp split: if_split_asm)
 apply ( drule field_fields)
 apply ( drule (1) fields_is_type)
 apply (  simp (no_asm_simp))
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/NanoJava/Example.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -184,7 +184,7 @@
 apply   rule
 apply   (rule hoare_ehoare.Asm) (* 20 *)
 apply   (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
-apply  (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
+apply  (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
 apply rule
 apply (rule hoare_ehoare.Call) (* 21 *)
 apply   (rule hoare_ehoare.LAcc)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nat.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1940,19 +1940,19 @@
 
 lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l"
   for m n l :: nat
-  by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
+  by (auto dest: less_imp_le less_imp_Suc_add split: nat_diff_split)
 
 lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m"
   for m n l :: nat
-  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
+  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split: nat_diff_split)
 
 lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
   for m n l :: nat
-  by (auto dest: less_imp_Suc_add split add: nat_diff_split)
+  by (auto dest: less_imp_Suc_add split: nat_diff_split)
 
 lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
   for m n :: nat
-  by (simp split add: nat_diff_split)
+  by (simp split: nat_diff_split)
 
 lemma min_diff: "min (m - i) (n - i) = min m n - i"
   for m n i :: nat
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nat_Transfer.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -1,4 +1,3 @@
-
 (* Authors: Jeremy Avigad and Amine Chaieb *)
 
 section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
@@ -82,7 +81,7 @@
 text \<open>first-order quantifiers\<close>
 
 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
-  by (simp split add: split_nat)
+  by (simp split: split_nat)
 
 lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
 proof
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Nonstandard_Analysis/HyperDef.thy
--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -285,7 +285,7 @@
 by (simp add: abs_if)
 
 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = \<bar>x + - z\<bar> ==> y = z | x = y"
-by (simp add: abs_if split add: if_split_asm)
+by (simp add: abs_if split: if_split_asm)
 
 
 subsection\<open>Embedding the Naturals into the Hyperreals\<close>
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -32,35 +32,35 @@
 
 lemma nat_diff_add_eq1:
      "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
-by (simp split add: nat_diff_split add: add_mult_distrib)
+by (simp split: nat_diff_split add: add_mult_distrib)
 
 lemma nat_diff_add_eq2:
      "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
-by (simp split add: nat_diff_split add: add_mult_distrib)
+by (simp split: nat_diff_split add: add_mult_distrib)
 
 lemma nat_eq_add_iff1:
      "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
 
 lemma nat_eq_add_iff2:
      "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
 
 lemma nat_less_add_iff1:
      "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
 
 lemma nat_less_add_iff2:
      "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
 
 lemma nat_le_add_iff1:
      "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
 
 lemma nat_le_add_iff2:
      "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
 
 text \<open>For \<open>cancel_numeral_factors\<close>\<close>
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Option.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -100,13 +100,13 @@
   by (auto split: option.split)
 
 lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
-  by (simp add: map_option_case split add: option.split)
+  by (simp add: map_option_case split: option.split)
 
 lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
 by(cases x) simp_all
 
 lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
-  by (simp add: map_option_case split add: option.split)
+  by (simp add: map_option_case split: option.split)
 
 lemma map_option_o_case_sum [simp]:
     "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Power.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -112,7 +112,7 @@
 
 lemma power_minus_mult:
   "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
-  by (simp add: power_commutes split add: nat_diff_split)
+  by (simp add: power_commutes split: nat_diff_split)
 
 end
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/SET_Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -493,7 +493,7 @@
 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
 
 
@@ -513,7 +513,7 @@
 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)
@@ -690,7 +690,7 @@
 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)
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/SET_Protocol/Public_SET.thy
--- 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
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -41,7 +41,7 @@
 
 lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
 apply (rule ext)
-apply (auto split add: nat_diff_split)
+apply (auto split: nat_diff_split)
 done
 
 subsection\<open>Injectiveness proof\<close>
@@ -120,7 +120,7 @@
        else if i<j then insert_map j t (f(i:=s))  
        else insert_map j t (f(i - Suc 0 := s)))"
 apply (rule ext) 
-apply (simp split add: nat_diff_split)
+apply (simp split: nat_diff_split)
  txt\<open>This simplification is VERY slow\<close>
 done
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -94,7 +94,7 @@
 
 lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
 apply (rule single_LeadsTo_I)
-apply (simp split add: if_split_asm)
+apply (simp split: if_split_asm)
 apply (rule MA1 [THEN Always_LeadsToI])
 apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto)
 done
@@ -147,7 +147,7 @@
   ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}  
                            \<inter> nmsg_eq 0 e)    \<subseteq>  final"
 apply (unfold final_def Equality_def)
-apply (auto split add: if_split_asm)
+apply (auto split!: if_split)
 apply (frule E_imp_in_V_L, blast)
 done
 
@@ -197,7 +197,7 @@
        (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
 apply (unfold final_def)
 apply (rule subset_antisym, blast)
-apply (auto split add: if_split_asm)
+apply (auto split: if_split_asm)
 apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
 done
 
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -82,7 +82,7 @@
      "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
 apply (unfold nodeOrder_def next_def)
 apply (auto simp add: mod_Suc mod_geq)
-apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
+apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
 done
 
 text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
diff -r 437bd400d808 -r f9f3006a5579 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -300,7 +300,7 @@
   "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
   apply (induct xs)
    apply simp
-  apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
+  apply (clarsimp simp add : nth_append nth.simps split: nat.split)
   apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
   apply arith
   done
@@ -577,11 +577,11 @@
 
 lemma take_takefill':
   "!!w n.  n = k + m ==> take k (takefill fill n w) = takefill fill k w"
-  by (induct k) (auto split add : list.split) 
+  by (induct k) (auto split: list.split) 
 
 lemma drop_takefill:
   "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
-  by (induct k) (auto split add : list.split) 
+  by (induct k) (auto split: list.split) 
 
 lemma takefill_le [simp]:
   "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
diff -r 437bd400d808 -r f9f3006a5579 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/ArithSimp.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -542,7 +542,7 @@
 
 lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i"
 apply (erule rev_mp)
-apply (simp split add: nat_diff_split, auto)
+apply (simp split: nat_diff_split, auto)
  apply (blast intro: add_le_self lt_trans1)
 apply (rule not_le_iff_lt [THEN iffD1], auto)
 apply (subgoal_tac "i #+ da < j #+ d", force)
@@ -552,7 +552,7 @@
 lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)"
 apply (frule le_in_nat, assumption)
 apply (frule lt_nat_in_nat, assumption)
-apply (simp split add: nat_diff_split, auto)
+apply (simp split: nat_diff_split, auto)
   apply (blast intro: lt_asym lt_trans2)
  apply (blast intro: lt_irrefl lt_trans2)
 apply (rule not_le_iff_lt [THEN iffD1], auto)
diff -r 437bd400d808 -r f9f3006a5579 src/ZF/IntDiv_ZF.thy
--- a/src/ZF/IntDiv_ZF.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/IntDiv_ZF.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -531,7 +531,7 @@
 apply assumption+
 apply (case_tac "#0 $< ba")
  apply (simp add: posDivAlg_eqn adjust_def integ_of_type
-             split add: split_if_asm)
+             split: split_if_asm)
  apply clarify
  apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
 apply (simp add: not_zless_iff_zle)
@@ -625,7 +625,7 @@
 apply assumption+
 apply (case_tac "#0 $< ba")
  apply (simp add: negDivAlg_eqn adjust_def integ_of_type
-             split add: split_if_asm)
+             split: split_if_asm)
  apply clarify
  apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
 apply (simp add: not_zless_iff_zle)
diff -r 437bd400d808 -r f9f3006a5579 src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/Int_ZF.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -283,7 +283,7 @@
 by (simp add: nat_of_def)
 
 lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
-by (auto simp add: congruent_def split add: nat_diff_split)
+by (auto simp add: congruent_def split: nat_diff_split)
 
 lemma raw_nat_of:
     "[| x\<in>nat;  y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
@@ -367,7 +367,7 @@
 apply (subgoal_tac "intify(z) \<in> int")
 apply (simp add: int_def)
 apply (auto simp add: znegative nat_of_def raw_nat_of
-            split add: nat_diff_split)
+            split: nat_diff_split)
 done
 
 
diff -r 437bd400d808 -r f9f3006a5579 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/OrderType.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -517,7 +517,7 @@
 done
 
 lemma oadd_lt_cancel2: "[| i++j < i++k;  Ord(j) |] ==> j<k"
-apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split: split_if_asm)
  prefer 2
  apply (frule_tac i = i and j = j in oadd_le_self)
  apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
@@ -530,7 +530,7 @@
 by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
 
 lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
-apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp add: oadd_eq_if_raw_oadd split: split_if_asm)
 apply (simp add: raw_oadd_eq_oadd)
 apply (rule Ord_linear_lt, auto)
 apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
@@ -538,7 +538,7 @@
 
 lemma lt_oadd_disj: "k < i++j ==> k<i | (\<exists>l\<in>j. k = i++l )"
 apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
-            split add: split_if_asm)
+            split: split_if_asm)
  prefer 2
  apply (simp add: Ord_in_Ord' [of _ j] lt_def)
 apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
diff -r 437bd400d808 -r f9f3006a5579 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -314,7 +314,7 @@
 apply (rule LeadsTo_weaken)
 apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
 prefer 3 apply assumption
-apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
+apply (auto split: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
 apply (blast dest: lt_asym)
 apply (force dest: add_lt_elim2)
 done
@@ -416,7 +416,7 @@
 apply (subgoal_tac "x`available_tok =
                     NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
 apply (simp add: )
-apply (auto split add: nat_diff_split dest: lt_trans2)
+apply (auto split: nat_diff_split dest: lt_trans2)
 done
 
 
diff -r 437bd400d808 -r f9f3006a5579 src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -489,7 +489,7 @@
 apply (force simp add: le_subset_iff, safe)
 apply (subgoal_tac "length (xs) #+ (i #- length (xs)) = i")
 apply (subst nth_drop)
-apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
+apply (simp_all (no_asm_simp) add: leI split: nat_diff_split)
 done
 
 lemma prefix_snoc: