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



On Tue, 23 Oct 2012, Ondřej Kunčar wrote:

ML source is not the real documentation!

You also need to include its history.

It is a matter of long practice and endurance to make sense out of all that. It is important to make a serious start, by giving up what you think about it in the first impulse.


	Makarius


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