src/HOL/Nat.thy
changeset 63648 f9f3006a5579
parent 63588 d0e2bad67bd4
child 63979 95c3ae4baba8
     1.1 --- a/src/HOL/Nat.thy	Tue Aug 09 23:29:54 2016 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Aug 10 09:33:54 2016 +0200
     1.3 @@ -1940,19 +1940,19 @@
     1.4  
     1.5  lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l"
     1.6    for m n l :: nat
     1.7 -  by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
     1.8 +  by (auto dest: less_imp_le less_imp_Suc_add split: nat_diff_split)
     1.9  
    1.10  lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m"
    1.11    for m n l :: nat
    1.12 -  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
    1.13 +  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split: nat_diff_split)
    1.14  
    1.15  lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
    1.16    for m n l :: nat
    1.17 -  by (auto dest: less_imp_Suc_add split add: nat_diff_split)
    1.18 +  by (auto dest: less_imp_Suc_add split: nat_diff_split)
    1.19  
    1.20  lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
    1.21    for m n :: nat
    1.22 -  by (simp split add: nat_diff_split)
    1.23 +  by (simp split: nat_diff_split)
    1.24  
    1.25  lemma min_diff: "min (m - i) (n - i) = min m n - i"
    1.26    for m n i :: nat