From: Tobias Nipkow <nip...@in.tum.de>
Date: Tue, 23 Oct 2012 11:31:11 UTC
Local: Tues, Oct 23 2012 7:31 am
Subject: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
I just tried my suggestion and it seems to break HOL. I'll investigate more.
Am 23/10/2012 13:17, schrieb Makarius:
> On Tue, 23 Oct 2012, Tobias Nipkow wrote:
>> "A conversion is any function that maps a term t to a theorem |-t==u."
>> up to beta-equivalence. Since conversions are low-level proof methods which
> Alternatively one could do the normalization before on the input term.
> Again, I don't expect too many fundamental problems in this rather small
> (Next time I will tell a story how an efficient and fully verified merge-sort
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.