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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
