*To*: Tjark Weber <tjark.weber at gmx.de>*Subject*: Re: [isabelle] The method "insert"*From*: John Ridgway <jridgway at wesleyan.edu>*Date*: Wed, 1 Nov 2006 10:06:42 -0500*Cc*: Fulya <fulyahorozal at gmail.com>, John Ridgway <jridgway at wesleyan.edu>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <200611011109.05655.tjark.weber@gmx.de>*References*: <68d9dc2d0610310612n4b52f7f2v5acdbe00036c31df@mail.gmail.com> <68d9dc2d0610310803y461fb0cbv4fd163fcb78ec9e5@mail.gmail.com> <200611011109.05655.tjark.weber@gmx.de>

Peace - john On Nov 1, 2006, at 5:09 AM, Tjark Weber wrote:

Fulya, On Tuesday 31 October 2006 17:03, Fulya wrote:lemma example333alem1:"real_lower_bound_of (underlying_set_of_sequence (%(n::nat). (1 /(sqrt(real n))))) 0" oops ... lemma example333a: "lim (%(n::nat). (1 / (sqrt (real n)))) = 0" apply (insert example333alem1)The error given in the proof of the lemma "example333a" is asfollows:Error in method "Pure.insert": *** Unknown theorem(s) "example333alem1" *** At command "apply". Could anyone give a solution to that error?"oops" aborts a proof attempt, so quite naturally example333alem1isn'tavailable afterwards. Try to "insert" a lemma that you have actually proved. Best, Tjark

**References**:**Re: [isabelle] The method "insert"***From:*Tjark Weber

- Previous by Date: Re: [isabelle] question about isar's HOL/Algebra
- Next by Date: [isabelle] Conditional interpretations?
- Previous by Thread: Re: [isabelle] The method "insert"
- Next by Thread: [isabelle] Conditional interpretations?
- Cl-isabelle-users November 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list