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. http://afp.hg.sourceforge.net/hgweb/afp/afp/file/e9fa38f86b76/thys/Binomial-Heaps/SkewBinomialHeap.thy#l1643). 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? Cheers, 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
