Re: [isabelle] "PROOF FAILED for depth4"



 > 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 appreciated.

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".

Alex





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