# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1547124684 0
# Node ID 6836da75b3ac04ad566c383b0729415f1c613e2b
# Parent  8b55240e12c6087f6641dafee2125b6b2946f24a
updated to Isabelle 2016-1

diff -r 8b55240e12c6 -r 6836da75b3ac thys2/Recs.thy
--- a/thys2/Recs.thy	Thu Jan 10 12:48:43 2019 +0000
+++ b/thys2/Recs.thy	Thu Jan 10 12:51:24 2019 +0000
@@ -44,8 +44,8 @@
 by (simp add:lessThan_Suc mult_ac)
 
 lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
-  setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}"
-  apply(subst setsum.union_disjoint[symmetric])
+  sum f {..<n} + sum f {n..p} = sum f {..p::nat}"
+  apply(subst sum.union_disjoint[symmetric])
   apply(auto simp add: ivl_disj_un_one)
 done
 
@@ -133,7 +133,7 @@
   have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" 
     using h2 by auto
   have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)"
-    using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) 
+    using h1 by (metis atLeast0LessThan le0 sum_add_nat_ivl) 
   also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp
   finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp
 qed