[isabelle-dev] Hooks for postprocessing sessions!?

[Lukas Bulwahn]

Hi Florian,

this sounds  similar to ideas that (Alex and) Lars had to allow 
find_theorems to search on all Isabelle sessions. As far as I know, they 
have an implementation for this feature in their shelf.


Lukas

On 10/11/2012 02:44 PM, Florian Haftmann wrote:
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121011/004fe03b/attachment-0002.html>