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