[isabelle-dev] State of affairs with simplifier tracing?

[Makarius]

On Thu, 27 Aug 2015, Florian Haftmann wrote:

> Currently, we have two simplifier tracing implementations, the classical
> one and the »new« one, which according to isar-ref still presents itself
> as a non-replacing alternative.
>
> What are the plans to continue from there?  This also affects derived
> functionality like tracing of code equation preprocessing.

This thread is still open, and won't be closed for Isabelle2016.

We should nonetheless make another effort soon.


 	Makarius