Re: [isabelle] Termination Proof
On Sun, Dec 19, 2010 at 3:20 AM, Alexander Krauss <krauss at in.tum.de> wrote:
> Hi Jason,
> theory Termination
>> imports Nat Multiset Divides Datatype
> First, you should import Parity, which already has the "even" predicate.
> And as Tobias said, if you don't import Main, you may not get the tools you
> expect, just some unfinished pieces lying around.
Thanks, that's good to know. I must have overlooked this advice in the
Isabelle tutorial as I don't recall hearing it before.
> Hope this helps...
Yes, your email was very helpful. I was able to get the proof to go through
and learned a bit about how it works in the process. I hope to send a
follow up email soon, as I have a few more questions now. I'm a bit short on
time at the moment so it may not be till the new year.
This archive was generated by a fusion of
Pipermail (Mailman edition) and