<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Hi Florian,<br>
<br>
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.<br>
<br>
<br>
Lukas<br>
<br>
On 10/11/2012 02:44 PM, Florian Haftmann wrote:
<blockquote cite="mid:5076BF25.6030204@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">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.
<a class="moz-txt-link-freetext" href="http://afp.hg.sourceforge.net/hgweb/afp/afp/file/e9fa38f86b76/thys/Binomial-Heaps/SkewBinomialHeap.thy#l1643">http://afp.hg.sourceforge.net/hgweb/afp/afp/file/e9fa38f86b76/thys/Binomial-Heaps/SkewBinomialHeap.thy#l1643</a>).
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
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>