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

Makarius makarius at sketis.net
Sat Jan 9 16:55:23 CET 2016

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.


More information about the isabelle-dev mailing list