Re: [isabelle] Termination Proof

On Sun, Dec 19, 2010 at 3:20 AM, Alexander Krauss <krauss at> 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 MHonArc.