diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Limits.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -22,7 +22,7 @@
      (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
 
 lemma at_infinity_eq_at_top_bot:
-  "(at_infinity \<Colon> real filter) = sup at_top at_bot"
+  "(at_infinity :: real filter) = sup at_top at_bot"
   apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
                    eventually_at_top_linorder eventually_at_bot_linorder)
   apply safe
@@ -872,7 +872,7 @@
   using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
 
 lemma filterlim_at_infinity:
-  fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
+  fixes f :: "_ \<Rightarrow> 'a::real_normed_vector"
   assumes "0 \<le> c"
   shows "(LIM x F. f x :> at_infinity) \<longleftrightarrow> (\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F)"
   unfolding filterlim_iff eventually_at_infinity
@@ -983,7 +983,7 @@
 qed
 
 lemma tendsto_inverse_0:
-  fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
+  fixes x :: "_ \<Rightarrow> 'a::real_normed_div_algebra"
   shows "(inverse ---> (0::'a)) at_infinity"
   unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity
 proof safe
@@ -1041,7 +1041,7 @@
   unfolding filterlim_def at_top_to_right filtermap_filtermap ..
 
 lemma filterlim_inverse_at_infinity:
-  fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
+  fixes x :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}"
   shows "filterlim inverse at_infinity (at (0::'a))"
   unfolding filterlim_at_infinity[OF order_refl]
 proof safe
@@ -1053,7 +1053,7 @@
 qed
 
 lemma filterlim_inverse_at_iff:
-  fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring}"
+  fixes g :: "'a \<Rightarrow> 'b::{real_normed_div_algebra, division_ring}"
   shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)"
   unfolding filterlim_def filtermap_filtermap[symmetric]
 proof
@@ -1078,7 +1078,7 @@
 
 
 lemma at_to_infinity:
-  fixes x :: "'a \<Colon> {real_normed_field,field}"
+  fixes x :: "'a :: {real_normed_field,field}"
   shows "(at (0::'a)) = filtermap inverse at_infinity"
 proof (rule antisym)
   have "(inverse ---> (0::'a)) at_infinity"
@@ -1226,7 +1226,7 @@
 qed
 
 lemma tendsto_divide_0:
-  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
+  fixes f :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}"
   assumes f: "(f ---> c) F"
   assumes g: "LIM x F. g x :> at_infinity"
   shows "((\<lambda>x. f x / g x) ---> 0) F"