diff -r 69e30a7e8880 -r 1b2acb3ccb29 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Tue May 22 17:56:06 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Tue May 22 19:47:55 2007 +0200
@@ -160,8 +160,8 @@
 by (fold real_norm_def, rule LIM_norm_zero_iff)
 
 lemma LIM_const_not_eq:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
 apply (simp add: LIM_eq)
 apply (rule_tac x="norm (k - L)" in exI, simp, safe)
 apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
@@ -170,16 +170,16 @@
 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
 
 lemma LIM_const_eq:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "(%x. k) -- a --> L ==> k = L"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
 apply (rule ccontr)
 apply (blast dest: LIM_const_not_eq)
 done
 
 lemma LIM_unique:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
-apply (drule LIM_diff, assumption)
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
+apply (drule (1) LIM_diff)
 apply (auto dest!: LIM_const_eq)
 done