Re: [isabelle] Browsing Main?



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  (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!






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.