Re: [isabelle] The method "insert"



You could try using "sorry" instead of "oops", as "sorry" does not abort the proof attempt.

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 as follows:

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 example333alem1 isn't
available afterwards.  Try to "insert" a lemma that you have actually
proved.

Best,
Tjark






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