Hi Florian,
Thanks for all this.
2. Meanwhile, I really like the new simplifier tracing facility and
hardly ever use the old [[simp_trace]]. Since the new trace offers a lot
of control over the tracing, would it make sense to base the tracing
facility on the new one?
It would definitely make
Hi Andreas,
Sorry for the long delay until you get an answer, but I wanted to wait
until I can port my application from Isabelle2013-2 to 2014. The tracing
facility seems to provide some basic means to limit the scope of the
tracing. I found the two suggestions for improvement:
1. The
Hi Florian,
Sorry for the long delay until you get an answer, but I wanted to wait until I can port my
application from Isabelle2013-2 to 2014. The tracing facility seems to provide some basic
means to limit the scope of the tracing. I found the two suggestions for improvement:
1. The
Hi Andreas,
with http://isabelle.in.tum.de/repos/isabelle/rev/020cea57eaa4 I have
provided very basic means to trace the code preprocessor. Alas, I only
dimly remember what your real requirements are, so feel free to comment
on it. Anyway, it is a starting point.
Cheers,
Florian
--
