Re: [isabelle] Browsing Main?
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
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:
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...
This archive was generated by a fusion of
Pipermail (Mailman edition) and