diff -r 8eb6365f5916 -r b9a1486e79be src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Nat_Transfer.thy	Mon Oct 17 11:46:22 2016 +0200
@@ -186,13 +186,13 @@
 ]
 
 
-text \<open>setsum and setprod\<close>
+text \<open>sum and setprod\<close>
 
 (* this handles the case where the *domain* of f is nat *)
 lemma transfer_nat_int_sum_prod:
-    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
+    "sum f A = sum (%x. f (nat x)) (int ` A)"
     "setprod f A = setprod (%x. f (nat x)) (int ` A)"
-  apply (subst setsum.reindex)
+  apply (subst sum.reindex)
   apply (unfold inj_on_def, auto)
   apply (subst setprod.reindex)
   apply (unfold inj_on_def o_def, auto)
@@ -200,17 +200,17 @@
 
 (* this handles the case where the *range* of f is nat *)
 lemma transfer_nat_int_sum_prod2:
-    "setsum f A = nat(setsum (%x. int (f x)) A)"
+    "sum f A = nat(sum (%x. int (f x)) A)"
     "setprod f A = nat(setprod (%x. int (f x)) A)"
-  apply (simp only: int_setsum [symmetric] nat_int)
+  apply (simp only: int_sum [symmetric] nat_int)
   apply (simp only: int_setprod [symmetric] nat_int)
   done
 
 lemma transfer_nat_int_sum_prod_closure:
-    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   unfolding nat_set_def
-  apply (rule setsum_nonneg)
+  apply (rule sum_nonneg)
   apply auto
   apply (rule setprod_nonneg)
   apply auto
@@ -222,10 +222,10 @@
   also: what does =simp=> do?
 
 lemma transfer_nat_int_sum_prod_closure:
-    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   unfolding nat_set_def simp_implies_def
-  apply (rule setsum_nonneg)
+  apply (rule sum_nonneg)
   apply auto
   apply (rule setprod_nonneg)
   apply auto
@@ -233,16 +233,16 @@
 *)
 
 (* Making A = B in this lemma doesn't work. Why not?
-   Also, why aren't setsum.cong and setprod.cong enough,
+   Also, why aren't sum.cong and setprod.cong enough,
    with the previously mentioned rule turned on? *)
 
 lemma transfer_nat_int_sum_prod_cong:
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
-      setsum f A = setsum g B"
+      sum f A = sum g B"
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
       setprod f A = setprod g B"
   unfolding nat_set_def
-  apply (subst setsum.cong, assumption)
+  apply (subst sum.cong, assumption)
   apply auto [2]
   apply (subst setprod.cong, assumption, auto)
 done
@@ -389,13 +389,13 @@
 ]
 
 
-text \<open>setsum and setprod\<close>
+text \<open>sum and setprod\<close>
 
 (* this handles the case where the *domain* of f is int *)
 lemma transfer_int_nat_sum_prod:
-    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
+    "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
     "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
-  apply (subst setsum.reindex)
+  apply (subst sum.reindex)
   apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
   apply (subst setprod.reindex)
   apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
@@ -404,14 +404,14 @@
 
 (* this handles the case where the *range* of f is int *)
 lemma transfer_int_nat_sum_prod2:
-    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
+    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
       setprod f A = int(setprod (%x. nat (f x)) A)"
   unfolding is_nat_def
-  by (subst int_setsum) auto
+  by (subst int_sum) auto
 
 declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
-  cong: setsum.cong setprod.cong]
+  cong: sum.cong setprod.cong]
 
 end