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



On Tue, 23 Oct 2012, Tobias Nipkow wrote:

I just tried my suggestion and it seems to break HOL. I'll investigate more.

I would have given it a > 50% chance of not breaking immediately, since rewrite_conv is relatively new back in Isabelle/HOL.

Anyway, whoever thinks something needs to be changed in a certain way, the first move is to make some empirical studies to test the hypothesis against historical reality.


	Makarius





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