[isabelle-dev] Hooks for postprocessing sessions!?

Lars Noschinski noschinl at in.tum.de
Thu Oct 11 17:30:45 CEST 2012


On 11.10.2012 17:00, Makarius wrote:
> On Thu, 11 Oct 2012, Lukas Bulwahn wrote:
>
>> 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.
>
> I was wondering about that recently. So far the only visible result was
> an unclear status of find_theorems.ML (e.g. in Isabelle/e3945ddcb9aa).
> At some point I would like to see find_theorems.scala as well.

I never got around to add the whole thing to the Isabelle repository. 
This is partly related to the fact, that I only have an hackish way to 
hook into the build process and generate the index. I always wanted to 
revisit this. I'll set it on my list for after the next paper deadline.

   -- Lars



More information about the isabelle-dev mailing list