[isabelle] The method "insert"

Dear Isabelle users,

I am trying to construct a proof for an example in Isabelle regarding
I am having a problem to apply the method "insert" in the proof.
Here is the formalized example:
 real_lower_bound_of :: "real set => real => bool"
 "real_lower_bound_of S u == \<forall>s \<in> S. u \<le> s"

 inf :: "real set => real"
 "inf S == THE x. (is_infimum_of S x)"

 underlying_set_of_sequence :: "(nat => real) => real set"
 " underlying_set_of_sequence X == {x. \<exists>(n::nat). (X n)=x}"
lemma example333alem1:
"real_lower_bound_of (underlying_set_of_sequence (%(n::nat). (1 / (sqrt
(real n))))) 0"
lemma example333a:
"lim (%(n::nat). (1 / (sqrt (real n)))) = 0"
apply (insert example333alem1)


The error given in the proof of the lemma "example333a" is as follows:

Error in method "Pure.insert":
*** Unknown theorem(s) "example333alem1"
*** At command "apply".

Could anyone give a solution to that error?
Thanks a lot!

Fulya Horozal
Saarland University
Saarbruecken, Germany

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.