From: Lawrence Paulson <l...@cam.ac.uk>
Date: Tue, 23 Oct 2012 14:19:58 UTC
Local: Tues, Oct 23 2012 10:19 am
Subject: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue
That application is very interesting! And one can argue that a simproc is a very similar concept as a conversion, anyway.
On 23 Oct 2012, at 14:41, Brian Huffman <huff...@in.tum.de> wrote:
> On Tue, Oct 23, 2012 at 3:21 PM, Lawrence Paulson <l...@cam.ac.uk> wrote:
>> As a historical remark, I'm quite attached to conversions, which were the topic of my very first journal article:
>> L. C. Paulson.
>> They made a lot of sense in the context of LCF and HOL, where users routinely wrote code as part of the verification process. Although I included this code in Isabelle, it didn't have a central role and I thought it'd got deleted. Obviously it would be sensible to correct any deficiencies or omissions. But I'm still intrigued regarding what sort of application you could have for them.
> I can't speak for Peter, but I am currently using conversions in a few places.
> My main application is for writing simprocs: See e.g.
> I would definitely recommend conversions to anyone thinking about
> I am also using conversions inside the transfer package, to do some
> - Brian
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.