Email Gateway (Aug 18 2022 at 19:55): Email Gateway (Aug 18 2022 at 19:55):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 18 2022 at 19:58):From: Brian Huffman <huffman@in.tum.de>
It is better to start your web browsing one level up, at
http://isabelle.in.tum.de/dist/library/HOL/
where you are one click away from seeing any ancestor theory of Main.
Or are you asking for something else?
Email Gateway (Aug 18 2022 at 19:59):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 18 2022 at 20:00):From: Alfio Martini <alfio.martini@acm.org>
Hi Brian,
This suffices if all these theories are really included in Main. I was not
so sure of this, especially
after reading this:
theory Main
imports Plain Predicate_Compile Nitpick SMT
begin
Also, this was not clear from the tutorial and the pdf documentation of
Main. Looking at the dependency theory graph, I have impression that we
have in the ancessor list above more theories that there are (really) in
Main.
Thus, what I really wanted is to browse (examine?) Main exactly in the way
I can do, for
instance, for Datatype.
But I do not know if this could be done. It seems that Main is actually
created "under the hood".
Many thanks for the reply!
Email Gateway (Aug 18 2022 at 20:01):From: Alfio Martini <alfio.martini@acm.org>
I finally got it! :-)
Best!
Last updated: Nov 21 2024 at 12:39 UTC