[isabelle-dev] Hooks for postprocessing sessions!?
bulwahn at in.tum.de
Thu Oct 11 15:28:51 CEST 2012
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.
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.
> 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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev