"split add" -> "split"
authornipkow
Wed Aug 10 09:33:54 2016 +0200 (2016-08-10)
changeset 63648f9f3006a5579
parent 63647 437bd400d808
child 63649 e690d6f2185b
child 63650 50cadecbe5bc
"split add" -> "split"
src/Doc/Tutorial/Inductive/AB.thy
src/Doc/Tutorial/Protocol/Event.thy
src/Doc/Tutorial/Protocol/Public.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/State.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Binomial.thy
src/HOL/Deriv.thy
src/HOL/Finite_Set.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/HOLCF/IOA/NTP/Lemmas.thy
src/HOL/HOLCF/IOA/RefCorrectness.thy
src/HOL/HOLCF/IOA/Seq.thy
src/HOL/HOLCF/IOA/SimCorrectness.thy
src/HOL/HOLCF/IOA/TL.thy
src/HOL/HOLCF/IOA/TLS.thy
src/HOL/IOA/Solve.thy
src/HOL/Int.thy
src/HOL/Library/positivstellensatz.ML
src/HOL/Map.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/NanoJava/Example.thy
src/HOL/Nat.thy
src/HOL/Nat_Transfer.thy
src/HOL/Nonstandard_Analysis/HyperDef.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Option.thy
src/HOL/Power.thy
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/SET_Protocol/Public_SET.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/Simple/Token.thy
src/HOL/Word/Bool_List_Representation.thy
src/ZF/ArithSimp.thy
src/ZF/IntDiv_ZF.thy
src/ZF/Int_ZF.thy
src/ZF/OrderType.thy
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/GenPrefix.thy
     1.1 --- a/src/Doc/Tutorial/Inductive/AB.thy	Tue Aug 09 23:29:54 2016 +0200
     1.2 +++ b/src/Doc/Tutorial/Inductive/AB.thy	Wed Aug 10 09:33:54 2016 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4  *}
     1.5  
     1.6    apply(force simp add: min_less_iff_disj)
     1.7 - apply(force split add: nat_diff_split)
     1.8 + apply(force split: nat_diff_split)
     1.9  
    1.10  txt{*
    1.11  The case @{prop"w = b#v"} is proved analogously:
    1.12 @@ -278,7 +278,7 @@
    1.13  apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
    1.14  apply(rule S_A_B.intros)
    1.15   apply(force simp add: min_less_iff_disj)
    1.16 -by(force simp add: min_less_iff_disj split add: nat_diff_split)
    1.17 +by(force simp add: min_less_iff_disj split: nat_diff_split)
    1.18  
    1.19  text{*
    1.20  We conclude this section with a comparison of our proof with 
     2.1 --- a/src/Doc/Tutorial/Protocol/Event.thy	Tue Aug 09 23:29:54 2016 +0200
     2.2 +++ b/src/Doc/Tutorial/Protocol/Event.thy	Wed Aug 10 09:33:54 2016 +0200
     2.3 @@ -125,13 +125,13 @@
     2.4  lemma Says_imp_knows_Spy [rule_format]:
     2.5       "Says A B X \<in> set evs --> X \<in> knows Spy evs"
     2.6  apply (induct_tac "evs")
     2.7 -apply (simp_all (no_asm_simp) split add: event.split)
     2.8 +apply (simp_all (no_asm_simp) split: event.split)
     2.9  done
    2.10  
    2.11  lemma Notes_imp_knows_Spy [rule_format]:
    2.12       "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
    2.13  apply (induct_tac "evs")
    2.14 -apply (simp_all (no_asm_simp) split add: event.split)
    2.15 +apply (simp_all (no_asm_simp) split: event.split)
    2.16  done
    2.17  
    2.18  
    2.19 @@ -174,14 +174,14 @@
    2.20  text{*Agents know what they say*}
    2.21  lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
    2.22  apply (induct_tac "evs")
    2.23 -apply (simp_all (no_asm_simp) split add: event.split)
    2.24 +apply (simp_all (no_asm_simp) split: event.split)
    2.25  apply blast
    2.26  done
    2.27  
    2.28  text{*Agents know what they note*}
    2.29  lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
    2.30  apply (induct_tac "evs")
    2.31 -apply (simp_all (no_asm_simp) split add: event.split)
    2.32 +apply (simp_all (no_asm_simp) split: event.split)
    2.33  apply blast
    2.34  done
    2.35  
    2.36 @@ -189,7 +189,7 @@
    2.37  lemma Gets_imp_knows_agents [rule_format]:
    2.38       "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
    2.39  apply (induct_tac "evs")
    2.40 -apply (simp_all (no_asm_simp) split add: event.split)
    2.41 +apply (simp_all (no_asm_simp) split: event.split)
    2.42  done
    2.43  
    2.44  
    2.45 @@ -200,7 +200,7 @@
    2.46    Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
    2.47  apply (erule rev_mp)
    2.48  apply (induct_tac "evs")
    2.49 -apply (simp_all (no_asm_simp) split add: event.split)
    2.50 +apply (simp_all (no_asm_simp) split: event.split)
    2.51  apply blast
    2.52  done
    2.53  
    2.54 @@ -211,7 +211,7 @@
    2.55    Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
    2.56  apply (erule rev_mp)
    2.57  apply (induct_tac "evs")
    2.58 -apply (simp_all (no_asm_simp) split add: event.split)
    2.59 +apply (simp_all (no_asm_simp) split: event.split)
    2.60  apply blast
    2.61  done
    2.62  
    2.63 @@ -224,7 +224,7 @@
    2.64  
    2.65  lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
    2.66  apply (induct_tac "evs")
    2.67 -apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
    2.68 +apply (simp_all add: parts_insert_knows_A split: event.split, blast)
    2.69  done
    2.70  
    2.71  lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
     3.1 --- a/src/Doc/Tutorial/Protocol/Public.thy	Tue Aug 09 23:29:54 2016 +0200
     3.2 +++ b/src/Doc/Tutorial/Protocol/Public.thy	Wed Aug 10 09:33:54 2016 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4  lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
     3.5  apply (induct_tac "evs")
     3.6  apply (rule_tac x = 0 in exI)
     3.7 -apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
     3.8 +apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
     3.9  apply safe
    3.10  apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
    3.11  done
     4.1 --- a/src/HOL/Auth/Event.thy	Tue Aug 09 23:29:54 2016 +0200
     4.2 +++ b/src/HOL/Auth/Event.thy	Wed Aug 10 09:33:54 2016 +0200
     4.3 @@ -124,13 +124,13 @@
     4.4  lemma Says_imp_knows_Spy [rule_format]:
     4.5       "Says A B X \<in> set evs --> X \<in> knows Spy evs"
     4.6  apply (induct_tac "evs")
     4.7 -apply (simp_all (no_asm_simp) split add: event.split)
     4.8 +apply (simp_all (no_asm_simp) split: event.split)
     4.9  done
    4.10  
    4.11  lemma Notes_imp_knows_Spy [rule_format]:
    4.12       "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
    4.13  apply (induct_tac "evs")
    4.14 -apply (simp_all (no_asm_simp) split add: event.split)
    4.15 +apply (simp_all (no_asm_simp) split: event.split)
    4.16  done
    4.17  
    4.18  
    4.19 @@ -164,14 +164,14 @@
    4.20  text\<open>Agents know what they say\<close>
    4.21  lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
    4.22  apply (induct_tac "evs")
    4.23 -apply (simp_all (no_asm_simp) split add: event.split)
    4.24 +apply (simp_all (no_asm_simp) split: event.split)
    4.25  apply blast
    4.26  done
    4.27  
    4.28  text\<open>Agents know what they note\<close>
    4.29  lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
    4.30  apply (induct_tac "evs")
    4.31 -apply (simp_all (no_asm_simp) split add: event.split)
    4.32 +apply (simp_all (no_asm_simp) split: event.split)
    4.33  apply blast
    4.34  done
    4.35  
    4.36 @@ -179,7 +179,7 @@
    4.37  lemma Gets_imp_knows_agents [rule_format]:
    4.38       "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
    4.39  apply (induct_tac "evs")
    4.40 -apply (simp_all (no_asm_simp) split add: event.split)
    4.41 +apply (simp_all (no_asm_simp) split: event.split)
    4.42  done
    4.43  
    4.44  
    4.45 @@ -190,7 +190,7 @@
    4.46    Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
    4.47  apply (erule rev_mp)
    4.48  apply (induct_tac "evs")
    4.49 -apply (simp_all (no_asm_simp) split add: event.split)
    4.50 +apply (simp_all (no_asm_simp) split: event.split)
    4.51  apply blast
    4.52  done
    4.53  
    4.54 @@ -201,7 +201,7 @@
    4.55    Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
    4.56  apply (erule rev_mp)
    4.57  apply (induct_tac "evs")
    4.58 -apply (simp_all (no_asm_simp) split add: event.split)
    4.59 +apply (simp_all (no_asm_simp) split: event.split)
    4.60  apply blast
    4.61  done
    4.62  
    4.63 @@ -214,7 +214,7 @@
    4.64  
    4.65  lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
    4.66  apply (induct_tac "evs")
    4.67 -apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
    4.68 +apply (simp_all add: parts_insert_knows_A split: event.split, blast)
    4.69  done
    4.70  
    4.71  lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
     5.1 --- a/src/HOL/Auth/Public.thy	Tue Aug 09 23:29:54 2016 +0200
     5.2 +++ b/src/HOL/Auth/Public.thy	Wed Aug 10 09:33:54 2016 +0200
     5.3 @@ -309,7 +309,7 @@
     5.4  text\<open>All public keys are visible\<close>
     5.5  lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
     5.6  apply (induct_tac "evs")
     5.7 -apply (auto simp add: imageI knows_Cons split add: event.split)
     5.8 +apply (auto simp add: imageI knows_Cons split: event.split)
     5.9  done
    5.10  
    5.11  lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
    5.12 @@ -319,14 +319,14 @@
    5.13  lemma Spy_spies_bad_privateKey [intro!]:
    5.14       "A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
    5.15  apply (induct_tac "evs")
    5.16 -apply (auto simp add: imageI knows_Cons split add: event.split)
    5.17 +apply (auto simp add: imageI knows_Cons split: event.split)
    5.18  done
    5.19  
    5.20  text\<open>Spy sees long-term shared keys of bad agents!\<close>
    5.21  lemma Spy_spies_bad_shrK [intro!]:
    5.22       "A \<in> bad ==> Key (shrK A) \<in> spies evs"
    5.23  apply (induct_tac "evs")
    5.24 -apply (simp_all add: imageI knows_Cons split add: event.split)
    5.25 +apply (simp_all add: imageI knows_Cons split: event.split)
    5.26  done
    5.27  
    5.28  lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
    5.29 @@ -361,7 +361,7 @@
    5.30  lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
    5.31  apply (induct_tac "evs")
    5.32  apply (rule_tac x = 0 in exI)
    5.33 -apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
    5.34 +apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
    5.35  apply safe
    5.36  apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
    5.37  done
     6.1 --- a/src/HOL/Auth/Shared.thy	Tue Aug 09 23:29:54 2016 +0200
     6.2 +++ b/src/HOL/Auth/Shared.thy	Wed Aug 10 09:33:54 2016 +0200
     6.3 @@ -78,7 +78,7 @@
     6.4  (*Spy sees shared keys of agents!*)
     6.5  lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
     6.6  apply (induct_tac "evs")
     6.7 -apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
     6.8 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
     6.9  done
    6.10  
    6.11  (*For case analysis on whether or not an agent is compromised*)
    6.12 @@ -123,7 +123,7 @@
    6.13  lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
    6.14  apply (induct_tac "evs")
    6.15  apply (rule_tac x = 0 in exI)
    6.16 -apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
    6.17 +apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
    6.18  apply (metis le_sup_iff msg_Nonce_supply)
    6.19  done
    6.20  
     7.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Tue Aug 09 23:29:54 2016 +0200
     7.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Wed Aug 10 09:33:54 2016 +0200
     7.3 @@ -196,13 +196,13 @@
     7.4  lemma Says_imp_knows_Spy [rule_format]:
     7.5       "Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
     7.6  apply (induct_tac "evs")
     7.7 -apply (simp_all (no_asm_simp) split add: event.split)
     7.8 +apply (simp_all (no_asm_simp) split: event.split)
     7.9  done
    7.10  
    7.11  lemma Notes_imp_knows_Spy [rule_format]:
    7.12       "Notes A X \<in> set evs \<longrightarrow> A\<in> bad \<longrightarrow> X \<in> knows Spy evs"
    7.13  apply (induct_tac "evs")
    7.14 -apply (simp_all (no_asm_simp) split add: event.split)
    7.15 +apply (simp_all (no_asm_simp) split: event.split)
    7.16  done
    7.17  
    7.18  (*Nothing can be stated on a Gets event*)
    7.19 @@ -210,13 +210,13 @@
    7.20  lemma Inputs_imp_knows_Spy_secureM [rule_format (no_asm)]: 
    7.21       "Inputs Spy C X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
    7.22  apply (induct_tac "evs")
    7.23 -apply (simp_all (no_asm_simp) split add: event.split)
    7.24 +apply (simp_all (no_asm_simp) split: event.split)
    7.25  done
    7.26  
    7.27  lemma Inputs_imp_knows_Spy_insecureM [rule_format (no_asm)]:
    7.28       "Inputs A C X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
    7.29  apply (induct_tac "evs")
    7.30 -apply (simp_all (no_asm_simp) split add: event.split)
    7.31 +apply (simp_all (no_asm_simp) split: event.split)
    7.32  done
    7.33  
    7.34  (*Nothing can be stated on a C_Gets event*)
    7.35 @@ -224,13 +224,13 @@
    7.36  lemma Outpts_imp_knows_Spy_secureM [rule_format (no_asm)]: 
    7.37       "Outpts C Spy X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
    7.38  apply (induct_tac "evs")
    7.39 -apply (simp_all (no_asm_simp) split add: event.split)
    7.40 +apply (simp_all (no_asm_simp) split: event.split)
    7.41  done
    7.42  
    7.43  lemma Outpts_imp_knows_Spy_insecureM [rule_format (no_asm)]:
    7.44       "Outpts C A X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
    7.45  apply (induct_tac "evs")
    7.46 -apply (simp_all (no_asm_simp) split add: event.split)
    7.47 +apply (simp_all (no_asm_simp) split: event.split)
    7.48  done
    7.49  
    7.50  (*Nothing can be stated on an A_Gets event*)
    7.51 @@ -290,14 +290,14 @@
    7.52  text\<open>Agents know what they say\<close>
    7.53  lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
    7.54  apply (induct_tac "evs")
    7.55 -apply (simp_all (no_asm_simp) split add: event.split)
    7.56 +apply (simp_all (no_asm_simp) split: event.split)
    7.57  apply blast
    7.58  done
    7.59  
    7.60  text\<open>Agents know what they note\<close>
    7.61  lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
    7.62  apply (induct_tac "evs")
    7.63 -apply (simp_all (no_asm_simp) split add: event.split)
    7.64 +apply (simp_all (no_asm_simp) split: event.split)
    7.65  apply blast
    7.66  done
    7.67  
    7.68 @@ -305,14 +305,14 @@
    7.69  lemma Gets_imp_knows_agents [rule_format]:
    7.70       "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
    7.71  apply (induct_tac "evs")
    7.72 -apply (simp_all (no_asm_simp) split add: event.split)
    7.73 +apply (simp_all (no_asm_simp) split: event.split)
    7.74  done
    7.75  
    7.76  (*Agents know what they input to their smart card*)
    7.77  lemma Inputs_imp_knows_agents [rule_format (no_asm)]: 
    7.78       "Inputs A (Card A) X \<in> set evs \<longrightarrow> X \<in> knows A evs"
    7.79  apply (induct_tac "evs")
    7.80 -apply (simp_all (no_asm_simp) split add: event.split)
    7.81 +apply (simp_all (no_asm_simp) split: event.split)
    7.82  apply blast
    7.83  done
    7.84  
    7.85 @@ -323,14 +323,14 @@
    7.86  lemma Outpts_imp_knows_agents_secureM [rule_format (no_asm)]: 
    7.87       "secureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
    7.88  apply (induct_tac "evs")
    7.89 -apply (simp_all (no_asm_simp) split add: event.split)
    7.90 +apply (simp_all (no_asm_simp) split: event.split)
    7.91  done
    7.92  
    7.93  (*otherwise only the spy knows the outputs*)
    7.94  lemma Outpts_imp_knows_agents_insecureM [rule_format (no_asm)]: 
    7.95        "insecureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
    7.96  apply (induct_tac "evs")
    7.97 -apply (simp_all (no_asm_simp) split add: event.split)
    7.98 +apply (simp_all (no_asm_simp) split: event.split)
    7.99  done
   7.100  
   7.101  (*end lemmas about agents' knowledge*)
   7.102 @@ -346,7 +346,7 @@
   7.103  
   7.104  lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs"
   7.105  apply (induct_tac "evs")
   7.106 -apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
   7.107 +apply (simp_all add: parts_insert_knows_A split: event.split, blast)
   7.108  done
   7.109  
   7.110  simps_of_case used_Cons_simps[simp]: used_Cons
   7.111 @@ -362,28 +362,28 @@
   7.112  lemma Says_parts_used [rule_format (no_asm)]: 
   7.113       "Says A B X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   7.114  apply (induct_tac "evs")
   7.115 -apply (simp_all (no_asm_simp) split add: event.split)
   7.116 +apply (simp_all (no_asm_simp) split: event.split)
   7.117  apply blast
   7.118  done
   7.119  
   7.120  lemma Notes_parts_used [rule_format (no_asm)]: 
   7.121       "Notes A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   7.122  apply (induct_tac "evs")
   7.123 -apply (simp_all (no_asm_simp) split add: event.split)
   7.124 +apply (simp_all (no_asm_simp) split: event.split)
   7.125  apply blast
   7.126  done
   7.127  
   7.128  lemma Outpts_parts_used [rule_format (no_asm)]: 
   7.129       "Outpts C A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   7.130  apply (induct_tac "evs")
   7.131 -apply (simp_all (no_asm_simp) split add: event.split)
   7.132 +apply (simp_all (no_asm_simp) split: event.split)
   7.133  apply blast
   7.134  done
   7.135  
   7.136  lemma Inputs_parts_used [rule_format (no_asm)]: 
   7.137       "Inputs A C X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   7.138  apply (induct_tac "evs")
   7.139 -apply (simp_all (no_asm_simp) split add: event.split)
   7.140 +apply (simp_all (no_asm_simp) split: event.split)
   7.141  apply blast
   7.142  done
   7.143  
     8.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Tue Aug 09 23:29:54 2016 +0200
     8.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Aug 10 09:33:54 2016 +0200
     8.3 @@ -137,7 +137,7 @@
     8.4  (*Spy knows the pins of bad agents!*)
     8.5  lemma Spy_knows_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
     8.6  apply (induct_tac "evs")
     8.7 -apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
     8.8 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
     8.9  done
    8.10  
    8.11  (*Spy knows the long-term keys of cloned cards!*)
    8.12 @@ -147,24 +147,24 @@
    8.13                             Key (pin A)  \<in> knows Spy evs &  
    8.14                            (\<forall> B. Key (pairK(B,A)) \<in> knows Spy evs)"
    8.15  apply (induct_tac "evs")
    8.16 -apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
    8.17 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
    8.18  done
    8.19  
    8.20  lemma Spy_knows_cloned1 [intro!]: "C \<in> cloned \<Longrightarrow> Key (crdK C) \<in> knows Spy evs"
    8.21  apply (induct_tac "evs")
    8.22 -apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
    8.23 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
    8.24  done
    8.25  
    8.26  lemma Spy_knows_cloned2 [intro!]: "\<lbrakk> Card A \<in> cloned; Card B \<in> cloned \<rbrakk>  
    8.27     \<Longrightarrow> Nonce (Pairkey(A,B))\<in> knows Spy evs"
    8.28  apply (induct_tac "evs")
    8.29 -apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
    8.30 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
    8.31  done
    8.32  
    8.33  (*Spy only knows pins of bad agents!*)
    8.34  lemma Spy_knows_Spy_bad [intro!]: "A\<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
    8.35  apply (induct_tac "evs")
    8.36 -apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
    8.37 +apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
    8.38  done
    8.39  
    8.40  
     9.1 --- a/src/HOL/Bali/AxCompl.thy	Tue Aug 09 23:29:54 2016 +0200
     9.2 +++ b/src/HOL/Bali/AxCompl.thy	Wed Aug 10 09:33:54 2016 +0200
     9.3 @@ -56,7 +56,7 @@
     9.4  
     9.5  lemma nyinitcls_init_lvars [simp]: 
     9.6    "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
     9.7 -  by (induct s) (simp add: init_lvars_def2 split add: if_split)
     9.8 +  by (induct s) (simp add: init_lvars_def2 split: if_split)
     9.9  
    9.10  lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
    9.11    unfolding nyinitcls_def by fast
    9.12 @@ -74,7 +74,7 @@
    9.13  apply  (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
    9.14  apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
    9.15  apply   (auto dest!: not_initedD elim!: 
    9.16 -              simp add: nyinitcls_def inited_def split add: if_split_asm)
    9.17 +              simp add: nyinitcls_def inited_def split: if_split_asm)
    9.18  done
    9.19  
    9.20  lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
    9.21 @@ -1072,7 +1072,7 @@
    9.22          apply (rule ax_derivs.NewA 
    9.23                 [where ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty T) 
    9.24                                \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"])
    9.25 -        apply  (simp add: init_comp_ty_def split add: if_split)
    9.26 +        apply  (simp add: init_comp_ty_def split: if_split)
    9.27          apply  (rule conjI, clarsimp)
    9.28          apply   (rule MGFn_InitD [OF hyp, THEN conseq2])
    9.29          apply   (clarsimp intro: eval.Init)
    10.1 --- a/src/HOL/Bali/Conform.thy	Tue Aug 09 23:29:54 2016 +0200
    10.2 +++ b/src/HOL/Bali/Conform.thy	Wed Aug 10 09:33:54 2016 +0200
    10.3 @@ -207,7 +207,7 @@
    10.4  apply (unfold lconf_def)
    10.5  apply safe
    10.6  apply (case_tac [3] "n")
    10.7 -apply (force split add: sum.split)+
    10.8 +apply (force split: sum.split)+
    10.9  done
   10.10  
   10.11  lemma lconf_ext_list [rule_format (no_asm)]: "
   10.12 @@ -288,7 +288,7 @@
   10.13  apply (unfold wlconf_def)
   10.14  apply safe
   10.15  apply (case_tac [3] "n")
   10.16 -apply (force split add: sum.split)+
   10.17 +apply (force split: sum.split)+
   10.18  done
   10.19  
   10.20  lemma wlconf_ext_list [rule_format (no_asm)]: "
   10.21 @@ -370,7 +370,7 @@
   10.22  apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
   10.23  defer
   10.24  apply (subst obj_ty_cong)
   10.25 -apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
   10.26 +apply (auto dest!: fields_table_SomeD split: sum.split_asm obj_tag.split_asm)
   10.27  done
   10.28  
   10.29  subsubsection "state conformance"
    11.1 --- a/src/HOL/Bali/Decl.thy	Tue Aug 09 23:29:54 2016 +0200
    11.2 +++ b/src/HOL/Bali/Decl.thy	Wed Aug 10 09:33:54 2016 +0200
    11.3 @@ -69,22 +69,22 @@
    11.4  proof
    11.5    fix x y z::acc_modi
    11.6    show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
    11.7 -    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
    11.8 +    by (auto simp add: le_acc_def less_acc_def split: acc_modi.split) 
    11.9    show "x \<le> x"                       \<comment> reflexivity
   11.10      by (auto simp add: le_acc_def)
   11.11    {
   11.12      assume "x \<le> y" "y \<le> z"           \<comment> transitivity 
   11.13      then show "x \<le> z"
   11.14 -      by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
   11.15 +      by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
   11.16    next
   11.17      assume "x \<le> y" "y \<le> x"           \<comment> antisymmetry
   11.18      moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
   11.19 -      by (auto simp add: less_acc_def split add: acc_modi.split)
   11.20 +      by (auto simp add: less_acc_def split: acc_modi.split)
   11.21      ultimately show "x = y" by (unfold le_acc_def) iprover
   11.22    next
   11.23      fix x y:: acc_modi
   11.24      show "x \<le> y \<or> y \<le> x"   
   11.25 -      by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
   11.26 +      by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
   11.27    }
   11.28  qed
   11.29    
    12.1 --- a/src/HOL/Bali/Eval.thy	Tue Aug 09 23:29:54 2016 +0200
    12.2 +++ b/src/HOL/Bali/Eval.thy	Wed Aug 10 09:33:54 2016 +0200
    12.3 @@ -1166,12 +1166,12 @@
    12.4        [strip_tac @{context}, rotate_tac ~1, eresolve_tac @{context} @{thms eval_elim_cases}])\<close>)
    12.5  (* 31 subgoals *)
    12.6  prefer 28 (* Try *) 
    12.7 -apply (simp (no_asm_use) only: split add: if_split_asm)
    12.8 +apply (simp (no_asm_use) only: split: if_split_asm)
    12.9  (* 34 subgoals *)
   12.10  prefer 30 (* Init *)
   12.11  apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+)
   12.12  prefer 26 (* While *)
   12.13 -apply (simp (no_asm_use) only: split add: if_split_asm, blast)
   12.14 +apply (simp (no_asm_use) only: split: if_split_asm, blast)
   12.15  (* 36 subgoals *)
   12.16  apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
   12.17  done
    13.1 --- a/src/HOL/Bali/State.thy	Tue Aug 09 23:29:54 2016 +0200
    13.2 +++ b/src/HOL/Bali/State.thy	Wed Aug 10 09:33:54 2016 +0200
    13.3 @@ -97,7 +97,7 @@
    13.4  lemma obj_ty_widenD: 
    13.5   "G\<turnstile>obj_ty obj\<preceq>RefT t \<Longrightarrow> (\<exists>C. tag obj = CInst C) \<or> (\<exists>T k. tag obj = Arr T k)"
    13.6  apply (unfold obj_ty_def)
    13.7 -apply (auto split add: obj_tag.split_asm)
    13.8 +apply (auto split: obj_tag.split_asm)
    13.9  done
   13.10  
   13.11  definition
   13.12 @@ -207,7 +207,7 @@
   13.13                   fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) nt 
   13.14                    = Some T))"
   13.15  apply (unfold var_tys_def arr_comps_def)
   13.16 -apply (force split add: sum.split_asm sum.split obj_tag.split)
   13.17 +apply (force split: sum.split_asm sum.split obj_tag.split)
   13.18  done
   13.19  
   13.20  
   13.21 @@ -704,7 +704,7 @@
   13.22  
   13.23  lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)"
   13.24  apply (unfold inited_def)
   13.25 -apply (auto split add: st.split)
   13.26 +apply (auto split: st.split)
   13.27  done
   13.28  
   13.29  lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))"
    14.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Aug 09 23:29:54 2016 +0200
    14.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Aug 10 09:33:54 2016 +0200
    14.3 @@ -213,7 +213,7 @@
    14.4  apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
    14.5   simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
    14.6              check_field_access_def check_method_access_def Let_def
    14.7 - split del: if_split_asm split add: sum3.split)
    14.8 + split del: if_split_asm split: sum3.split)
    14.9  (* 6 subgoals *)
   14.10  apply force+
   14.11  done
   14.12 @@ -632,7 +632,7 @@
   14.13  apply (case_tac "mode = IntVir")
   14.14  apply (drule conf_RefTD)
   14.15  apply (force intro!: conf_AddrI 
   14.16 -            simp add: obj_class_def split add: obj_tag.split_asm)
   14.17 +            simp add: obj_class_def split: obj_tag.split_asm)
   14.18  apply  clarsimp
   14.19  apply  safe
   14.20  apply    (erule (1) widen.subcls [THEN conf_widen])
   14.21 @@ -655,7 +655,7 @@
   14.22  
   14.23  lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
   14.24      x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
   14.25 -apply (auto split add: split_abrupt_if simp add: throw_def2)
   14.26 +apply (auto split: split_abrupt_if simp add: throw_def2)
   14.27  apply (erule conforms_xconf)
   14.28  apply (frule conf_RefTD)
   14.29  apply (auto elim: widen.subcls [THEN conf_widen])
   14.30 @@ -674,7 +674,7 @@
   14.31  "\<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);
   14.32    dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
   14.33  \<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
   14.34 -apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   14.35 +apply (auto elim: eval_gext' conforms_xgext split: split_abrupt_if)
   14.36  done
   14.37  
   14.38  lemma FVar_lemma1: 
   14.39 @@ -700,7 +700,7 @@
   14.40  apply  (erule fields_table_SomeI, simp (no_asm))
   14.41  apply clarsimp
   14.42  apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
   14.43 -apply (auto dest!: widen_Array split add: obj_tag.split)
   14.44 +apply (auto dest!: widen_Array split: obj_tag.split)
   14.45  apply (rule fields_table_SomeI)
   14.46  apply (auto elim!: fields_mono subcls_is_class2)
   14.47  done
   14.48 @@ -829,7 +829,7 @@
   14.49     =
   14.50    (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   14.51  apply (unfold lconf_def)
   14.52 -apply (auto split add: lname.splits)
   14.53 +apply (auto split: lname.splits)
   14.54  done
   14.55  
   14.56  lemma wlconf_map_lname [simp]: 
   14.57 @@ -837,7 +837,7 @@
   14.58     =
   14.59    (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   14.60  apply (unfold wlconf_def)
   14.61 -apply (auto split add: lname.splits)
   14.62 +apply (auto split: lname.splits)
   14.63  done
   14.64  
   14.65  lemma lconf_map_ename [simp]:
   14.66 @@ -845,7 +845,7 @@
   14.67     =
   14.68    (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   14.69  apply (unfold lconf_def)
   14.70 -apply (auto split add: ename.splits)
   14.71 +apply (auto split: ename.splits)
   14.72  done
   14.73  
   14.74  lemma wlconf_map_ename [simp]:
   14.75 @@ -853,7 +853,7 @@
   14.76     =
   14.77    (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   14.78  apply (unfold wlconf_def)
   14.79 -apply (auto split add: ename.splits)
   14.80 +apply (auto split: ename.splits)
   14.81  done
   14.82  
   14.83  
   14.84 @@ -902,7 +902,7 @@
   14.85                                then None else Some (Class declC)))"
   14.86  apply (simp add: init_lvars_def2)
   14.87  apply (rule conforms_set_locals)
   14.88 -apply  (simp (no_asm_simp) split add: if_split)
   14.89 +apply  (simp (no_asm_simp) split: if_split)
   14.90  apply (drule  (4) DynT_conf)
   14.91  apply clarsimp
   14.92  (* apply intro *)
    15.1 --- a/src/HOL/Binomial.thy	Tue Aug 09 23:29:54 2016 +0200
    15.2 +++ b/src/HOL/Binomial.thy	Wed Aug 10 09:33:54 2016 +0200
    15.3 @@ -317,7 +317,7 @@
    15.4  text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close>
    15.5  lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
    15.6    using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
    15.7 -  by (auto split add: nat_diff_split)
    15.8 +  by (auto split: nat_diff_split)
    15.9  
   15.10  
   15.11  subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>
    16.1 --- a/src/HOL/Deriv.thy	Tue Aug 09 23:29:54 2016 +0200
    16.2 +++ b/src/HOL/Deriv.thy	Wed Aug 10 09:33:54 2016 +0200
    16.3 @@ -1095,7 +1095,7 @@
    16.4      fix h :: real
    16.5      assume "0 < h" "h < s" "x - h \<in> S"
    16.6      with all [of "x - h"] show "f x < f (x-h)"
    16.7 -    proof (simp add: abs_if pos_less_divide_eq dist_real_def split add: if_split_asm)
    16.8 +    proof (simp add: abs_if pos_less_divide_eq dist_real_def split: if_split_asm)
    16.9        assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
   16.10        with l have "0 < (f (x-h) - f x) / h"
   16.11          by arith
    17.1 --- a/src/HOL/Finite_Set.thy	Tue Aug 09 23:29:54 2016 +0200
    17.2 +++ b/src/HOL/Finite_Set.thy	Wed Aug 10 09:33:54 2016 +0200
    17.3 @@ -1405,7 +1405,7 @@
    17.4    apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
    17.5     prefer 2 apply (blast intro: finite_subset, atomize)
    17.6    apply (drule_tac x = "A - {x}" in spec)
    17.7 -  apply (simp add: card_Diff_singleton_if split add: if_split_asm)
    17.8 +  apply (simp add: card_Diff_singleton_if split: if_split_asm)
    17.9    apply (case_tac "card A", auto)
   17.10    done
   17.11  
    18.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Aug 09 23:29:54 2016 +0200
    18.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Aug 10 09:33:54 2016 +0200
    18.3 @@ -155,14 +155,14 @@
    18.4  apply (rule impI)
    18.5  apply (erule conjE)+
    18.6  apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
    18.7 -  split add: if_split)
    18.8 +  split: if_split)
    18.9  txt \<open>detour 2\<close>
   18.10  apply (tactic "tac @{context} 1")
   18.11  apply (tactic "tac_ren @{context} 1")
   18.12  apply (rule impI)
   18.13  apply (erule conjE)+
   18.14  apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
   18.15 -  Multiset.delm_nonempty_def split add: if_split)
   18.16 +  Multiset.delm_nonempty_def split: if_split)
   18.17  apply (rule allI)
   18.18  apply (rule conjI)
   18.19  apply (rule impI)
    19.1 --- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Tue Aug 09 23:29:54 2016 +0200
    19.2 +++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Wed Aug 10 09:33:54 2016 +0200
    19.3 @@ -25,7 +25,7 @@
    19.4  subsection \<open>Arithmetic\<close>
    19.5  
    19.6  lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
    19.7 -  by (simp add: diff_Suc split add: nat.split)
    19.8 +  by (simp add: diff_Suc split: nat.split)
    19.9  
   19.10  lemmas [simp] = hd_append set_lemmas
   19.11  
    20.1 --- a/src/HOL/HOLCF/IOA/RefCorrectness.thy	Tue Aug 09 23:29:54 2016 +0200
    20.2 +++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy	Wed Aug 10 09:33:54 2016 +0200
    20.3 @@ -189,7 +189,7 @@
    20.4    apply (auto simp add: mk_traceConc)
    20.5    apply (frule reachable.reachable_n)
    20.6    apply assumption
    20.7 -  apply (auto simp add: move_subprop4 split add: if_split)
    20.8 +  apply (auto simp add: move_subprop4 split: if_split)
    20.9    done
   20.10  
   20.11  
    21.1 --- a/src/HOL/HOLCF/IOA/Seq.thy	Tue Aug 09 23:29:54 2016 +0200
    21.2 +++ b/src/HOL/HOLCF/IOA/Seq.thy	Wed Aug 10 09:33:54 2016 +0200
    21.3 @@ -5,7 +5,7 @@
    21.4  section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
    21.5  
    21.6  theory Seq
    21.7 -imports "../../HOLCF"
    21.8 +imports "../HOLCF"
    21.9  begin
   21.10  
   21.11  default_sort pcpo
    22.1 --- a/src/HOL/HOLCF/IOA/SimCorrectness.thy	Tue Aug 09 23:29:54 2016 +0200
    22.2 +++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy	Wed Aug 10 09:33:54 2016 +0200
    22.3 @@ -173,7 +173,7 @@
    22.4    apply (erule_tac x = "t" in allE)
    22.5    apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
    22.6    apply (simp add: move_subprop5_sim [unfolded Let_def]
    22.7 -    move_subprop4_sim [unfolded Let_def] split add: if_split)
    22.8 +    move_subprop4_sim [unfolded Let_def] split: if_split)
    22.9    done
   22.10  
   22.11  text \<open>Lemma 2: \<open>corresp_ex_sim\<close> is execution\<close>
    23.1 --- a/src/HOL/HOLCF/IOA/TL.thy	Tue Aug 09 23:29:54 2016 +0200
    23.2 +++ b/src/HOL/HOLCF/IOA/TL.thy	Wed Aug 10 09:33:54 2016 +0200
    23.3 @@ -128,7 +128,7 @@
    23.4    apply (erule_tac x = "s" in allE)
    23.5    apply (simp add: tsuffix_def suffix_refl)
    23.6    text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close>
    23.7 -  apply (simp split add: if_split)
    23.8 +  apply (simp split: if_split)
    23.9    apply auto
   23.10    apply (drule tsuffix_TL2)
   23.11    apply assumption+
    24.1 --- a/src/HOL/HOLCF/IOA/TLS.thy	Tue Aug 09 23:29:54 2016 +0200
    24.2 +++ b/src/HOL/HOLCF/IOA/TLS.thy	Wed Aug 10 09:33:54 2016 +0200
    24.3 @@ -140,7 +140,7 @@
    24.4                \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))"
    24.5    apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
    24.6    apply clarify
    24.7 -  apply (simp split add: if_split)
    24.8 +  apply (simp split: if_split)
    24.9    text \<open>\<open>TL = UU\<close>\<close>
   24.10    apply (rule conjI)
   24.11    apply (pair ex)
    25.1 --- a/src/HOL/IOA/Solve.thy	Tue Aug 09 23:29:54 2016 +0200
    25.2 +++ b/src/HOL/IOA/Solve.thy	Wed Aug 10 09:33:54 2016 +0200
    25.3 @@ -86,7 +86,7 @@
    25.4    apply (simp cong del: if_weak_cong
    25.5      add: executions_def is_execution_fragment_def par_def starts_of_def
    25.6        trans_of_def filter_oseq_def
    25.7 -    split add: option.split)
    25.8 +    split: option.split)
    25.9    done
   25.10  
   25.11  
   25.12 @@ -103,7 +103,7 @@
   25.13    apply (simp cong del: if_weak_cong
   25.14      add: executions_def is_execution_fragment_def par_def starts_of_def
   25.15      trans_of_def filter_oseq_def
   25.16 -    split add: option.split)
   25.17 +    split: option.split)
   25.18    done
   25.19  
   25.20  declare if_split [split del] if_weak_cong [cong del]
   25.21 @@ -143,7 +143,7 @@
   25.22  (* delete auxiliary subgoal *)
   25.23    prefer 2
   25.24    apply force
   25.25 -  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: if_split)
   25.26 +  apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split: if_split)
   25.27    apply (tactic \<open>
   25.28      REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
   25.29        asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1)\<close>)
   25.30 @@ -157,7 +157,7 @@
   25.31    apply (simp (no_asm))
   25.32  (* execution is indeed an execution of C *)
   25.33    apply (simp add: executions_def is_execution_fragment_def par_def
   25.34 -    starts_of_def trans_of_def rename_def split add: option.split)
   25.35 +    starts_of_def trans_of_def rename_def split: option.split)
   25.36    apply force
   25.37    done
   25.38  
   25.39 @@ -197,7 +197,7 @@
   25.40    apply assumption
   25.41    apply simp
   25.42  (* x is internal *)
   25.43 -  apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
   25.44 +  apply (simp (no_asm) cong add: conj_cong)
   25.45    apply (rule impI)
   25.46    apply (erule conjE)
   25.47    apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
    26.1 --- a/src/HOL/Int.thy	Tue Aug 09 23:29:54 2016 +0200
    26.2 +++ b/src/HOL/Int.thy	Wed Aug 10 09:33:54 2016 +0200
    26.3 @@ -1190,7 +1190,7 @@
    26.4  apply (case_tac "k = f (Suc n)")
    26.5  apply force
    26.6  apply (erule impE)
    26.7 - apply (simp add: abs_if split add: if_split_asm)
    26.8 + apply (simp add: abs_if split: if_split_asm)
    26.9  apply (blast intro: le_SucI)
   26.10  done
   26.11  
    27.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Aug 09 23:29:54 2016 +0200
    27.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Aug 10 09:33:54 2016 +0200
    27.3 @@ -266,7 +266,7 @@
    27.4    by auto};
    27.5  
    27.6  val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
    27.7 -  by (atomize (full)) (auto split add: abs_split)};
    27.8 +  by (atomize (full)) (auto split: abs_split)};
    27.9  
   27.10  val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
   27.11    by (atomize (full)) (cases "x <= y", auto simp add: max_def)};
    28.1 --- a/src/HOL/Map.thy	Tue Aug 09 23:29:54 2016 +0200
    28.2 +++ b/src/HOL/Map.thy	Wed Aug 10 09:33:54 2016 +0200
    28.3 @@ -312,7 +312,7 @@
    28.4  apply (induct xs)
    28.5   apply simp
    28.6  apply (rule ext)
    28.7 -apply (simp split add: option.split)
    28.8 +apply (simp split: option.split)
    28.9  done
   28.10  
   28.11  lemma finite_range_map_of_map_add:
    29.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Aug 09 23:29:54 2016 +0200
    29.2 +++ b/src/HOL/MicroJava/J/Example.thy	Wed Aug 10 09:33:54 2016 +0200
    29.3 @@ -191,7 +191,7 @@
    29.4  lemma class_tprgD: 
    29.5  "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"
    29.6  apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
    29.7 -apply (auto split add: if_split_asm simp add: map_of_Cons)
    29.8 +apply (auto split: if_split_asm simp add: map_of_Cons)
    29.9  done
   29.10  
   29.11  lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R"
    30.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 09 23:29:54 2016 +0200
    30.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Aug 10 09:33:54 2016 +0200
    30.3 @@ -234,7 +234,7 @@
    30.4  apply( erule conjI)
    30.5  apply( clarsimp)
    30.6  apply( drule eval_no_xcpt)
    30.7 -apply( simp split add: binop.split)
    30.8 +apply( simp split: binop.split)
    30.9  
   30.10  \<comment> "12 LAcc"
   30.11  apply simp
    31.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Tue Aug 09 23:29:54 2016 +0200
    31.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Aug 10 09:33:54 2016 +0200
    31.3 @@ -146,7 +146,7 @@
    31.4  lemma wf_cdecl_supD: 
    31.5  "!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
    31.6  apply (unfold ws_cdecl_def)
    31.7 -apply (auto split add: option.split_asm)
    31.8 +apply (auto split: option.split_asm)
    31.9  done
   31.10  
   31.11  lemma subcls_asym: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> (D, C) \<notin> (subcls1 G)^+"
   31.12 @@ -534,7 +534,7 @@
   31.13   apply (simp add: map_of_map)
   31.14   apply (clarify)
   31.15   apply (subst method_rec, assumption+)
   31.16 - apply (simp add: map_add_def map_of_map split add: option.split)
   31.17 + apply (simp add: map_add_def map_of_map split: option.split)
   31.18  done
   31.19  
   31.20  
   31.21 @@ -554,7 +554,7 @@
   31.22   apply (simp add: map_of_map)
   31.23   apply (clarify)
   31.24   apply (subst method_rec, assumption+)
   31.25 - apply (simp add: map_add_def map_of_map split add: option.split)
   31.26 + apply (simp add: map_add_def map_of_map split: option.split)
   31.27  done
   31.28  
   31.29  lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
    32.1 --- a/src/HOL/MicroJava/J/WellType.thy	Tue Aug 09 23:29:54 2016 +0200
    32.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Wed Aug 10 09:33:54 2016 +0200
    32.3 @@ -215,7 +215,7 @@
    32.4  apply (rule ty_expr_ty_exprs_wt_stmt.induct)
    32.5  apply auto
    32.6  apply (   erule typeof_empty_is_type)
    32.7 -apply (  simp split add: if_split_asm)
    32.8 +apply (  simp split: if_split_asm)
    32.9  apply ( drule field_fields)
   32.10  apply ( drule (1) fields_is_type)
   32.11  apply (  simp (no_asm_simp))
    33.1 --- a/src/HOL/NanoJava/Example.thy	Tue Aug 09 23:29:54 2016 +0200
    33.2 +++ b/src/HOL/NanoJava/Example.thy	Wed Aug 10 09:33:54 2016 +0200
    33.3 @@ -184,7 +184,7 @@
    33.4  apply   rule
    33.5  apply   (rule hoare_ehoare.Asm) (* 20 *)
    33.6  apply   (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
    33.7 -apply  (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
    33.8 +apply  (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
    33.9  apply rule
   33.10  apply (rule hoare_ehoare.Call) (* 21 *)
   33.11  apply   (rule hoare_ehoare.LAcc)
    34.1 --- a/src/HOL/Nat.thy	Tue Aug 09 23:29:54 2016 +0200
    34.2 +++ b/src/HOL/Nat.thy	Wed Aug 10 09:33:54 2016 +0200
    34.3 @@ -1940,19 +1940,19 @@
    34.4  
    34.5  lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l"
    34.6    for m n l :: nat
    34.7 -  by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
    34.8 +  by (auto dest: less_imp_le less_imp_Suc_add split: nat_diff_split)
    34.9  
   34.10  lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m"
   34.11    for m n l :: nat
   34.12 -  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
   34.13 +  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split: nat_diff_split)
   34.14  
   34.15  lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
   34.16    for m n l :: nat
   34.17 -  by (auto dest: less_imp_Suc_add split add: nat_diff_split)
   34.18 +  by (auto dest: less_imp_Suc_add split: nat_diff_split)
   34.19  
   34.20  lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
   34.21    for m n :: nat
   34.22 -  by (simp split add: nat_diff_split)
   34.23 +  by (simp split: nat_diff_split)
   34.24  
   34.25  lemma min_diff: "min (m - i) (n - i) = min m n - i"
   34.26    for m n i :: nat
    35.1 --- a/src/HOL/Nat_Transfer.thy	Tue Aug 09 23:29:54 2016 +0200
    35.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Aug 10 09:33:54 2016 +0200
    35.3 @@ -1,4 +1,3 @@
    35.4 -
    35.5  (* Authors: Jeremy Avigad and Amine Chaieb *)
    35.6  
    35.7  section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
    35.8 @@ -82,7 +81,7 @@
    35.9  text \<open>first-order quantifiers\<close>
   35.10  
   35.11  lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
   35.12 -  by (simp split add: split_nat)
   35.13 +  by (simp split: split_nat)
   35.14  
   35.15  lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
   35.16  proof
    36.1 --- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Tue Aug 09 23:29:54 2016 +0200
    36.2 +++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Wed Aug 10 09:33:54 2016 +0200
    36.3 @@ -285,7 +285,7 @@
    36.4  by (simp add: abs_if)
    36.5  
    36.6  lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = \<bar>x + - z\<bar> ==> y = z | x = y"
    36.7 -by (simp add: abs_if split add: if_split_asm)
    36.8 +by (simp add: abs_if split: if_split_asm)
    36.9  
   36.10  
   36.11  subsection\<open>Embedding the Naturals into the Hyperreals\<close>
    37.1 --- a/src/HOL/Numeral_Simprocs.thy	Tue Aug 09 23:29:54 2016 +0200
    37.2 +++ b/src/HOL/Numeral_Simprocs.thy	Wed Aug 10 09:33:54 2016 +0200
    37.3 @@ -32,35 +32,35 @@
    37.4  
    37.5  lemma nat_diff_add_eq1:
    37.6       "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
    37.7 -by (simp split add: nat_diff_split add: add_mult_distrib)
    37.8 +by (simp split: nat_diff_split add: add_mult_distrib)
    37.9  
   37.10  lemma nat_diff_add_eq2:
   37.11       "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
   37.12 -by (simp split add: nat_diff_split add: add_mult_distrib)
   37.13 +by (simp split: nat_diff_split add: add_mult_distrib)
   37.14  
   37.15  lemma nat_eq_add_iff1:
   37.16       "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
   37.17 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   37.18 +by (auto split: nat_diff_split simp add: add_mult_distrib)
   37.19  
   37.20  lemma nat_eq_add_iff2:
   37.21       "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
   37.22 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   37.23 +by (auto split: nat_diff_split simp add: add_mult_distrib)
   37.24  
   37.25  lemma nat_less_add_iff1:
   37.26       "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
   37.27 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   37.28 +by (auto split: nat_diff_split simp add: add_mult_distrib)
   37.29  
   37.30  lemma nat_less_add_iff2:
   37.31       "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
   37.32 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   37.33 +by (auto split: nat_diff_split simp add: add_mult_distrib)
   37.34  
   37.35  lemma nat_le_add_iff1:
   37.36       "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
   37.37 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   37.38 +by (auto split: nat_diff_split simp add: add_mult_distrib)
   37.39  
   37.40  lemma nat_le_add_iff2:
   37.41       "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
   37.42 -by (auto split add: nat_diff_split simp add: add_mult_distrib)
   37.43 +by (auto split: nat_diff_split simp add: add_mult_distrib)
   37.44  
   37.45  text \<open>For \<open>cancel_numeral_factors\<close>\<close>
   37.46  
    38.1 --- a/src/HOL/Option.thy	Tue Aug 09 23:29:54 2016 +0200
    38.2 +++ b/src/HOL/Option.thy	Wed Aug 10 09:33:54 2016 +0200
    38.3 @@ -100,13 +100,13 @@
    38.4    by (auto split: option.split)
    38.5  
    38.6  lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
    38.7 -  by (simp add: map_option_case split add: option.split)
    38.8 +  by (simp add: map_option_case split: option.split)
    38.9  
   38.10  lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
   38.11  by(cases x) simp_all
   38.12  
   38.13  lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
   38.14 -  by (simp add: map_option_case split add: option.split)
   38.15 +  by (simp add: map_option_case split: option.split)
   38.16  
   38.17  lemma map_option_o_case_sum [simp]:
   38.18      "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
    39.1 --- a/src/HOL/Power.thy	Tue Aug 09 23:29:54 2016 +0200
    39.2 +++ b/src/HOL/Power.thy	Wed Aug 10 09:33:54 2016 +0200
    39.3 @@ -112,7 +112,7 @@
    39.4  
    39.5  lemma power_minus_mult:
    39.6    "0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
    39.7 -  by (simp add: power_commutes split add: nat_diff_split)
    39.8 +  by (simp add: power_commutes split: nat_diff_split)
    39.9  
   39.10  end
   39.11  
    40.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Tue Aug 09 23:29:54 2016 +0200
    40.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Wed Aug 10 09:33:54 2016 +0200
    40.3 @@ -493,7 +493,7 @@
    40.4  lemma K_fresh_not_KeyCryptKey:
    40.5       "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
    40.6  apply (induct evs)
    40.7 -apply (auto simp add: parts_insert2 split add: event.split)
    40.8 +apply (auto simp add: parts_insert2 split: event.split)
    40.9  done
   40.10  
   40.11  
   40.12 @@ -513,7 +513,7 @@
   40.13  text\<open>Lemma for message 5: pubSK C is never used to encrypt Keys.\<close>
   40.14  lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
   40.15  apply (induct_tac "evs")
   40.16 -apply (auto simp add: parts_insert2 split add: event.split)
   40.17 +apply (auto simp add: parts_insert2 split: event.split)
   40.18  done
   40.19  
   40.20  text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
   40.21 @@ -690,7 +690,7 @@
   40.22  text\<open>Lemma for message 5: pubSK C is never used to encrypt Nonces.\<close>
   40.23  lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
   40.24  apply (induct_tac "evs")
   40.25 -apply (auto simp add: parts_insert2 split add: event.split)
   40.26 +apply (auto simp add: parts_insert2 split: event.split)
   40.27  done
   40.28  
   40.29  text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
    41.1 --- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Aug 09 23:29:54 2016 +0200
    41.2 +++ b/src/HOL/SET_Protocol/Public_SET.thy	Wed Aug 10 09:33:54 2016 +0200
    41.3 @@ -300,7 +300,7 @@
    41.4  text\<open>Spy knows all public keys\<close>
    41.5  lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
    41.6  apply (induct_tac "evs")
    41.7 -apply (simp_all add: imageI knows_Cons split add: event.split)
    41.8 +apply (simp_all add: imageI knows_Cons split: event.split)
    41.9  done
   41.10  
   41.11  declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
   41.12 @@ -324,7 +324,7 @@
   41.13  lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
   41.14  apply (induct_tac "evs")
   41.15  apply (rule_tac x = 0 in exI)
   41.16 -apply (simp_all add: used_Cons split add: event.split, safe)
   41.17 +apply (simp_all add: used_Cons split: event.split, safe)
   41.18  apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
   41.19  done
   41.20  
    42.1 --- a/src/HOL/UNITY/Lift_prog.thy	Tue Aug 09 23:29:54 2016 +0200
    42.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Wed Aug 10 09:33:54 2016 +0200
    42.3 @@ -41,7 +41,7 @@
    42.4  
    42.5  lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
    42.6  apply (rule ext)
    42.7 -apply (auto split add: nat_diff_split)
    42.8 +apply (auto split: nat_diff_split)
    42.9  done
   42.10  
   42.11  subsection\<open>Injectiveness proof\<close>
   42.12 @@ -120,7 +120,7 @@
   42.13         else if i<j then insert_map j t (f(i:=s))  
   42.14         else insert_map j t (f(i - Suc 0 := s)))"
   42.15  apply (rule ext) 
   42.16 -apply (simp split add: nat_diff_split)
   42.17 +apply (simp split: nat_diff_split)
   42.18   txt\<open>This simplification is VERY slow\<close>
   42.19  done
   42.20  
    43.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Aug 09 23:29:54 2016 +0200
    43.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Aug 10 09:33:54 2016 +0200
    43.3 @@ -94,7 +94,7 @@
    43.4  
    43.5  lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
    43.6  apply (rule single_LeadsTo_I)
    43.7 -apply (simp split add: if_split_asm)
    43.8 +apply (simp split: if_split_asm)
    43.9  apply (rule MA1 [THEN Always_LeadsToI])
   43.10  apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto)
   43.11  done
   43.12 @@ -147,7 +147,7 @@
   43.13    ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}  
   43.14                             \<inter> nmsg_eq 0 e)    \<subseteq>  final"
   43.15  apply (unfold final_def Equality_def)
   43.16 -apply (auto split add: if_split_asm)
   43.17 +apply (auto split!: if_split)
   43.18  apply (frule E_imp_in_V_L, blast)
   43.19  done
   43.20  
   43.21 @@ -197,7 +197,7 @@
   43.22         (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
   43.23  apply (unfold final_def)
   43.24  apply (rule subset_antisym, blast)
   43.25 -apply (auto split add: if_split_asm)
   43.26 +apply (auto split: if_split_asm)
   43.27  apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
   43.28  done
   43.29  
    44.1 --- a/src/HOL/UNITY/Simple/Token.thy	Tue Aug 09 23:29:54 2016 +0200
    44.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Wed Aug 10 09:33:54 2016 +0200
    44.3 @@ -82,7 +82,7 @@
    44.4       "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
    44.5  apply (unfold nodeOrder_def next_def)
    44.6  apply (auto simp add: mod_Suc mod_geq)
    44.7 -apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
    44.8 +apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
    44.9  done
   44.10  
   44.11  text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
    45.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Tue Aug 09 23:29:54 2016 +0200
    45.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Wed Aug 10 09:33:54 2016 +0200
    45.3 @@ -300,7 +300,7 @@
    45.4    "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
    45.5    apply (induct xs)
    45.6     apply simp
    45.7 -  apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
    45.8 +  apply (clarsimp simp add : nth_append nth.simps split: nat.split)
    45.9    apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
   45.10    apply arith
   45.11    done
   45.12 @@ -577,11 +577,11 @@
   45.13  
   45.14  lemma take_takefill':
   45.15    "!!w n.  n = k + m ==> take k (takefill fill n w) = takefill fill k w"
   45.16 -  by (induct k) (auto split add : list.split) 
   45.17 +  by (induct k) (auto split: list.split) 
   45.18  
   45.19  lemma drop_takefill:
   45.20    "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
   45.21 -  by (induct k) (auto split add : list.split) 
   45.22 +  by (induct k) (auto split: list.split) 
   45.23  
   45.24  lemma takefill_le [simp]:
   45.25    "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
    46.1 --- a/src/ZF/ArithSimp.thy	Tue Aug 09 23:29:54 2016 +0200
    46.2 +++ b/src/ZF/ArithSimp.thy	Wed Aug 10 09:33:54 2016 +0200
    46.3 @@ -542,7 +542,7 @@
    46.4  
    46.5  lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i"
    46.6  apply (erule rev_mp)
    46.7 -apply (simp split add: nat_diff_split, auto)
    46.8 +apply (simp split: nat_diff_split, auto)
    46.9   apply (blast intro: add_le_self lt_trans1)
   46.10  apply (rule not_le_iff_lt [THEN iffD1], auto)
   46.11  apply (subgoal_tac "i #+ da < j #+ d", force)
   46.12 @@ -552,7 +552,7 @@
   46.13  lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)"
   46.14  apply (frule le_in_nat, assumption)
   46.15  apply (frule lt_nat_in_nat, assumption)
   46.16 -apply (simp split add: nat_diff_split, auto)
   46.17 +apply (simp split: nat_diff_split, auto)
   46.18    apply (blast intro: lt_asym lt_trans2)
   46.19   apply (blast intro: lt_irrefl lt_trans2)
   46.20  apply (rule not_le_iff_lt [THEN iffD1], auto)
    47.1 --- a/src/ZF/IntDiv_ZF.thy	Tue Aug 09 23:29:54 2016 +0200
    47.2 +++ b/src/ZF/IntDiv_ZF.thy	Wed Aug 10 09:33:54 2016 +0200
    47.3 @@ -531,7 +531,7 @@
    47.4  apply assumption+
    47.5  apply (case_tac "#0 $< ba")
    47.6   apply (simp add: posDivAlg_eqn adjust_def integ_of_type
    47.7 -             split add: split_if_asm)
    47.8 +             split: split_if_asm)
    47.9   apply clarify
   47.10   apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
   47.11  apply (simp add: not_zless_iff_zle)
   47.12 @@ -625,7 +625,7 @@
   47.13  apply assumption+
   47.14  apply (case_tac "#0 $< ba")
   47.15   apply (simp add: negDivAlg_eqn adjust_def integ_of_type
   47.16 -             split add: split_if_asm)
   47.17 +             split: split_if_asm)
   47.18   apply clarify
   47.19   apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
   47.20  apply (simp add: not_zless_iff_zle)
    48.1 --- a/src/ZF/Int_ZF.thy	Tue Aug 09 23:29:54 2016 +0200
    48.2 +++ b/src/ZF/Int_ZF.thy	Wed Aug 10 09:33:54 2016 +0200
    48.3 @@ -283,7 +283,7 @@
    48.4  by (simp add: nat_of_def)
    48.5  
    48.6  lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
    48.7 -by (auto simp add: congruent_def split add: nat_diff_split)
    48.8 +by (auto simp add: congruent_def split: nat_diff_split)
    48.9  
   48.10  lemma raw_nat_of:
   48.11      "[| x\<in>nat;  y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
   48.12 @@ -367,7 +367,7 @@
   48.13  apply (subgoal_tac "intify(z) \<in> int")
   48.14  apply (simp add: int_def)
   48.15  apply (auto simp add: znegative nat_of_def raw_nat_of
   48.16 -            split add: nat_diff_split)
   48.17 +            split: nat_diff_split)
   48.18  done
   48.19  
   48.20  
    49.1 --- a/src/ZF/OrderType.thy	Tue Aug 09 23:29:54 2016 +0200
    49.2 +++ b/src/ZF/OrderType.thy	Wed Aug 10 09:33:54 2016 +0200
    49.3 @@ -517,7 +517,7 @@
    49.4  done
    49.5  
    49.6  lemma oadd_lt_cancel2: "[| i++j < i++k;  Ord(j) |] ==> j<k"
    49.7 -apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm)
    49.8 +apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split: split_if_asm)
    49.9   prefer 2
   49.10   apply (frule_tac i = i and j = j in oadd_le_self)
   49.11   apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
   49.12 @@ -530,7 +530,7 @@
   49.13  by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
   49.14  
   49.15  lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
   49.16 -apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
   49.17 +apply (simp add: oadd_eq_if_raw_oadd split: split_if_asm)
   49.18  apply (simp add: raw_oadd_eq_oadd)
   49.19  apply (rule Ord_linear_lt, auto)
   49.20  apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
   49.21 @@ -538,7 +538,7 @@
   49.22  
   49.23  lemma lt_oadd_disj: "k < i++j ==> k<i | (\<exists>l\<in>j. k = i++l )"
   49.24  apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
   49.25 -            split add: split_if_asm)
   49.26 +            split: split_if_asm)
   49.27   prefer 2
   49.28   apply (simp add: Ord_in_Ord' [of _ j] lt_def)
   49.29  apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
    50.1 --- a/src/ZF/UNITY/AllocImpl.thy	Tue Aug 09 23:29:54 2016 +0200
    50.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Wed Aug 10 09:33:54 2016 +0200
    50.3 @@ -314,7 +314,7 @@
    50.4  apply (rule LeadsTo_weaken)
    50.5  apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
    50.6  prefer 3 apply assumption
    50.7 -apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
    50.8 +apply (auto split: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
    50.9  apply (blast dest: lt_asym)
   50.10  apply (force dest: add_lt_elim2)
   50.11  done
   50.12 @@ -416,7 +416,7 @@
   50.13  apply (subgoal_tac "x`available_tok =
   50.14                      NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
   50.15  apply (simp add: )
   50.16 -apply (auto split add: nat_diff_split dest: lt_trans2)
   50.17 +apply (auto split: nat_diff_split dest: lt_trans2)
   50.18  done
   50.19  
   50.20  
    51.1 --- a/src/ZF/UNITY/GenPrefix.thy	Tue Aug 09 23:29:54 2016 +0200
    51.2 +++ b/src/ZF/UNITY/GenPrefix.thy	Wed Aug 10 09:33:54 2016 +0200
    51.3 @@ -489,7 +489,7 @@
    51.4  apply (force simp add: le_subset_iff, safe)
    51.5  apply (subgoal_tac "length (xs) #+ (i #- length (xs)) = i")
    51.6  apply (subst nth_drop)
    51.7 -apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
    51.8 +apply (simp_all (no_asm_simp) add: leI split: nat_diff_split)
    51.9  done
   51.10  
   51.11  lemma prefix_snoc: