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 rewriting with the simplifier can be traced, but I have not been > able to activate it for function transformers (as, e.g., in > Code_Target_Nat for 0/Suc). If tracing for function X is active, it > might be useful to display the set of equations before and after the > application of each function transformer.
See now http://isabelle.in.tum.de/reports/Isabelle/rev/d230e7075bcf > 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 sense, but at the moment I will not put any personal effort into this. Contributions welcome for review. Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
