src/HOL/Int.thy
 changeset 61204 3e491e34a62e parent 61169 4de9ff3ea29a child 61234 a9e6052188fa
```     1.1 --- a/src/HOL/Int.thy	Mon Sep 21 14:44:32 2015 +0200
1.2 +++ b/src/HOL/Int.thy	Mon Sep 21 19:52:13 2015 +0100
1.3 @@ -518,7 +518,7 @@
1.4  lemma int_cases3 [case_names zero pos neg]:
1.5    fixes k :: int
1.6    assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
1.7 -    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
1.8 +    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
1.9    shows "P"
1.10  proof (cases k "0::int" rule: linorder_cases)
1.11    case equal with assms(1) show P by simp
1.12 @@ -890,7 +890,7 @@
1.13    moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
1.14      using that by induct simp
1.15    ultimately show ?thesis by blast
1.16 -qed
1.17 +qed
1.18
1.19  lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
1.20  apply (rule sym)
```