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.

Thanks,
Jason




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