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)