src/HOL/Nat.thy
changeset 45931 99cf6e470816
parent 45833 033cb3a668b9
child 45933 ee70da42e08a
     1.1 --- a/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Dec 19 14:41:08 2011 +0100
     1.3 @@ -721,10 +721,10 @@
     1.4  by (rule monoI) simp
     1.5  
     1.6  lemma min_0L [simp]: "min 0 n = (0::nat)"
     1.7 -by (rule min_leastL) simp
     1.8 +by (rule min_absorb1) simp
     1.9  
    1.10  lemma min_0R [simp]: "min n 0 = (0::nat)"
    1.11 -by (rule min_leastR) simp
    1.12 +by (rule min_absorb2) simp
    1.13  
    1.14  lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
    1.15  by (simp add: mono_Suc min_of_mono)
    1.16 @@ -738,10 +738,10 @@
    1.17  by (simp split: nat.split)
    1.18  
    1.19  lemma max_0L [simp]: "max 0 n = (n::nat)"
    1.20 -by (rule max_leastL) simp
    1.21 +by (rule max_absorb2) simp
    1.22  
    1.23  lemma max_0R [simp]: "max n 0 = (n::nat)"
    1.24 -by (rule max_leastR) simp
    1.25 +by (rule max_absorb1) simp
    1.26  
    1.27  lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
    1.28  by (simp add: mono_Suc max_of_mono)