src/HOL/Library/RBT_Set.thy
changeset 64267 b9a1486e79be
parent 63649 e690d6f2185b
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -85,7 +85,7 @@
     1.4    "Pow = Pow" ..
     1.5  
     1.6  lemma [code, code del]:
     1.7 -  "setsum = setsum" ..
     1.8 +  "sum = sum" ..
     1.9  
    1.10  lemma [code, code del]:
    1.11    "setprod = setprod" ..
    1.12 @@ -673,13 +673,13 @@
    1.13    "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
    1.14    by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
    1.15  
    1.16 -lemma setsum_Set [code]:
    1.17 -  "setsum f (Set xs) = fold_keys (plus o f) xs 0"
    1.18 +lemma sum_Set [code]:
    1.19 +  "sum f (Set xs) = fold_keys (plus o f) xs 0"
    1.20  proof -
    1.21    have "comp_fun_commute (\<lambda>x. op + (f x))"
    1.22      by standard (auto simp: ac_simps)
    1.23    then show ?thesis 
    1.24 -    by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
    1.25 +    by (auto simp add: sum.eq_fold finite_fold_fold_keys o_def)
    1.26  qed
    1.27  
    1.28  lemma the_elem_set [code]: