Re: [isabelle] Browsing Main?
This suffices if all these theories are really included in Main. I was not
so sure of this, especially
after reading this:
imports Plain Predicate_Compile Nitpick SMT
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
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!
On Wed, May 2, 2012 at 2:12 AM, Brian Huffman <huffman at in.tum.de> wrote:
> On Wed, May 2, 2012 at 6:57 AM, Alfio Martini <alfio.martini at acm.org>
> > Dear Users,
> > Although we "all know" (via the pdf documentation available) what is in
> > 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?
> It is better to start your web browsing one level up, at
> where you are one click away from seeing any ancestor theory of Main.
> Or are you asking for something else?
> - Brian
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