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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and