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
```