Re: [isabelle] "PROOF FAILED for depth4"
On Thu, Apr 8, 2010 at 12:34 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> > lemma te_zero: "EX func t. func t = 0"
>> > proof (intro exI)
>> > show "F s = 0"
>> Thanks for the help. Unfortunately, I get an error from this, saying that
>> it can't solve goal by exported rule: F s = 0. Any hint on this will be
> You may need to add type annotations to make sure that the types in your
> lemma statement are not more general than you want. Switch on "Isabelle ->
> Settings -> Show Types".
I see. However, why can't the types in the lemma be more general even the
function is existentially quantified? Can't a' and b' be instantiated to
real for F s = 0 in the proof?
This archive was generated by a fusion of
Pipermail (Mailman edition) and