Re: [isabelle] Browsing Main?

I finally got it! :-)


On Wed, May 2, 2012 at 2:14 AM, Christian Sternagel <c-sterna at>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.)
> cheers
> chris
> On 05/02/2012 01:57 PM, Alfio Martini wrote:
>> Dear Users,
>> Although we "all know" (via the pdf documentation available) what is in
>> the
>> Main.thy, it would be nice to browse through it
>> directly at**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...
>> Best!

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 MHonArc.