Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue



On Mon, 22 Oct 2012, Lawrence Paulson wrote:

This module was written long ago for a specific, internal purpose and was never intended for general use, so it's hard to say what is a bug and what isn't. The beauty of conversions is that they are highly modular, so you can write your own primitives that do exactly what you want.

I think you refer to an even older version of the module, before my time working on the Isabelle code base. The current src/Pure/conv.ML is a reconstruction from historic sources and the HOL counterparts that was initiated by Amine Chaieb some years ago, and where I engaged myself as well in doing research on the old LCF/HOL sources. The we tried to push it forward in time into contemporary Isabelle use.


	Makarius





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