src/HOL/IntDef.thy
changeset 23438 dd824e86fa8a
parent 23431 25ca91279a9b
child 23477 f4b83f03cac9
     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 20 17:02:57 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 20 17:28:55 2007 +0200
     1.3 @@ -554,7 +554,8 @@
     1.4  qed
     1.5  
     1.6  lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
     1.7 -by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
     1.8 +by (cases z rule: eq_Abs_Integ)
     1.9 +   (simp add: nat le of_int Zero_int_def of_nat_diff)
    1.10  
    1.11  
    1.12  subsection{*The Set of Integers*}