Email Gateway (Aug 19 2022 at 16:43): Email Gateway (Aug 19 2022 at 16:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
In Isabelle2014, Isabelle/ML structure »Predicate_Compile«, there is a
quasi-option as low-level unsynchronized reference »present_graph«,
which allows to display some kind of dependency graph during a run of
the predicate compiler. It does neither appear in documentation nor in
source. Is there any real application of this?
The reason why I am asking is that this would need significant
de-obscurification and modernization to stay in the middle run, and
efforts could be saved by just dropping it silently.
Looking forward to your suggestions,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC