[isabelle-dev] Hooks for postprocessing sessions!?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 11 14:44:21 CEST 2012

Hi all,

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?



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121011/d2fad446/attachment.asc>

More information about the isabelle-dev mailing list