--- a/src/HOL/Int.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Int.thy Fri Jul 22 08:02:37 2016 +0200
@@ -633,13 +633,13 @@
case equal with assms(1) show P by simp
next
case greater
- then have "nat k > 0" by simp
- moreover from this have "k = int (nat k)" by auto
+ then have *: "nat k > 0" by simp
+ moreover from * have "k = int (nat k)" by auto
ultimately show P using assms(2) by blast
next
case less
- then have "nat (- k) > 0" by simp
- moreover from this have "k = - int (nat (- k))" by auto
+ then have *: "nat (- k) > 0" by simp
+ moreover from * have "k = - int (nat (- k))" by auto
ultimately show P using assms(3) by blast
qed