[isabelle] Predicate_Compile.present_graph



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.