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

On Tue, 23 Oct 2012, Peter Lammich wrote:

So what normalizations does instantiate_normalize do (beta?, eta?,
beta-eta?, how deep?). Looking at the source code does not really help

fun instantiate_normalize instpair th =
 Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR

Larry should be able to tell you.

It is again the same technique to let rule composition perform some normalization. The above function goes back to Stefan Berghofer, IIRC. I merely changed its name Drule.instantiate ~> Drule.instantiate_normalize recently, to make it a bit more explicit what was meant here.


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