summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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