Re: [isabelle] qed and done take long for large goal states



On 03/08/16 09:34, Andreas Lochbihler wrote:
> I have eta contraction enabled for printing as is the default.

This probably refers to the "eta_contract" attribute. It happens much
later when abstractions are pretty printed.

Abbreviations see the original, independently of this option.


	Makarius





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