src/HOL/Inequalities.thy
changeset 60758 d8d85a8172b5
parent 60167 9a97407488cd
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Inequalities.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Inequalities.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    case (Suc i)
     1.5    have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
     1.6    have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
     1.7 -  also have "\<dots> = \<Sum> {m..n-1} + n" using `m \<le> n`
     1.8 +  also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
     1.9      by(subst atLeastAtMostPlus1_int_conv) simp_all
    1.10    also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
    1.11      by(simp add: Suc(1)[OF 0])
    1.12 @@ -43,7 +43,7 @@
    1.13    hence "{m..<n} = {m..n-1}" by auto
    1.14    hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
    1.15    also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
    1.16 -    using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute)
    1.17 +    using assms \<open>m < n\<close> by (simp add: Setsum_Icc_nat mult.commute)
    1.18    finally show ?thesis .
    1.19  next
    1.20    assume "\<not> m < n" with assms show ?thesis by simp