[isabelle-dev] State of affairs with simplifier tracing?
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