src/HOL/Int.thy
changeset 63539 70d4d9e5707b
parent 62390 842917225d56
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Int.thy	Thu Jul 21 10:52:27 2016 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri Jul 22 08:02:37 2016 +0200
     1.3 @@ -633,13 +633,13 @@
     1.4    case equal with assms(1) show P by simp
     1.5  next
     1.6    case greater
     1.7 -  then have "nat k > 0" by simp
     1.8 -  moreover from this have "k = int (nat k)" by auto
     1.9 +  then have *: "nat k > 0" by simp
    1.10 +  moreover from * have "k = int (nat k)" by auto
    1.11    ultimately show P using assms(2) by blast
    1.12  next
    1.13    case less
    1.14 -  then have "nat (- k) > 0" by simp
    1.15 -  moreover from this have "k = - int (nat (- k))" by auto
    1.16 +  then have *: "nat (- k) > 0" by simp
    1.17 +  moreover from * have "k = - int (nat (- k))" by auto
    1.18    ultimately show P using assms(3) by blast
    1.19  qed
    1.20