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