Re: [isabelle] Browsing Main?
I finally got it! :-)
On Wed, May 2, 2012 at 2:14 AM, Christian Sternagel <c-sterna at jaist.ac.jp>wrote:
> Dear Aflio,
> Main.thy is not empty you have to follow the imports backwards. And since
> this is also what Isabelle does, it would be very misleading to present it
> as if everything was actually inside Main. E.g., it is possible to refer to
> constants and theorems using a theory name as prefix. What you suggest
> would imply that "Main.hd" should work (since "hd" is available after
> importing Main) but actually only "List.hd" will work.
> I agree that browsing is a bit inconvenient. Try browsing inside jEdit
> instead. If you press Ctrl and click on a constant (like "hd") you will
> directly jump to its definition. (Use Ctrl + Backtick to jump back to the
> previous file.)
> On 05/02/2012 01:57 PM, Alfio Martini wrote:
>> Dear Users,
>> Although we "all know" (via the pdf documentation available) what is in
>> Main.thy, it would be nice to browse through it
>> directly at http://isabelle.in.tum.de/**dist/library/HOL/Main.html<http://isabelle.in.tum.de/dist/library/HOL/Main.html> (and
>> thus seeing all the details in real Isabelle),
>> instead of visiting the contributing theories in a brute-force way. Since
>> the theory is somehow "empty" at the address above,
>> I wonder if something like this could be available in the next release?
>> I am assuming this request makes some sense after all...
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and