[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