Re: [isabelle] Browsing Main?



I finally got it! :-)

Best!

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