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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and