--- a/src/HOL/Limits.thy Mon Feb 08 19:53:49 2016 +0100
+++ b/src/HOL/Limits.thy Tue Feb 09 06:39:31 2016 +0100
@@ -620,6 +620,12 @@
shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
unfolding continuous_on_def by (auto intro: tendsto_setsum)
+instance nat :: topological_comm_monoid_add
+ proof qed (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
+
+instance int :: topological_comm_monoid_add
+ proof qed (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
+
subsubsection \<open>Addition and subtraction\<close>
instance real_normed_vector < topological_comm_monoid_add