Re: [isabelle] Browsing Main?



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!

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>
> 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?
>
> 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?
>
> - 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 MHonArc.