src/HOL/Nat.thy
changeset 32437 66f1a0dfe7d9
parent 31998 2c7a24f74db9
child 32456 341c83339aeb
     1.1 --- a/src/HOL/Nat.thy	Fri Aug 28 18:52:41 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Aug 28 19:15:59 2009 +0200
     1.3 @@ -1512,7 +1512,7 @@
     1.4  by (simp split add: nat_diff_split)
     1.5  
     1.6  lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
     1.7 -unfolding min_def by auto
     1.8 +by auto
     1.9  
    1.10  lemma inj_on_diff_nat: 
    1.11    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"