src/HOL/Nat.thy
changeset 26300 03def556e26e
parent 26149 6094349a4de9
child 26315 cb3badaa192e
     1.1 --- a/src/HOL/Nat.thy	Mon Mar 17 18:36:04 2008 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Mar 17 18:37:00 2008 +0100
     1.3 @@ -855,9 +855,6 @@
     1.4  
     1.5  subsubsection {* More results about difference *}
     1.6  
     1.7 -lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
     1.8 -by (induct m) simp_all
     1.9 -
    1.10  text {* Addition is the inverse of subtraction:
    1.11    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
    1.12  lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"