[isabelle-dev] Hooks for postprocessing sessions!?
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 11 14:44:21 CEST 2012
recently I had the idea to generate reports for all accessible Isabelle
sessions containing e.g.
* all constants (with types) declared in a session
* all types declared in a session
* all classes declared in a session
* all theorems declared via »theorem«
The rationale is that this would allow for a quick analysis especially
of the AFP to find out which generally useful »auxiliary« stuff is
hidden there (e.g.
Is there already feasible hook interface to hook in, e.g. in present.ML,
or can this only be done by an ad-hoc patch?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 259 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev