*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] 2014-RC1 issues*From*: Makarius <makarius at sketis.net>*Date*: Wed, 30 Jul 2014 22:42:42 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1406732628.2398.66.camel@lapbroy33>*References*: <1406708816.2398.53.camel@lapbroy33> <1406732628.2398.66.camel@lapbroy33>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 30 Jul 2014, Peter Lammich wrote:

The sidekick panel is supposed to show an overview of the theory. At the top-level of the hierarchy, you can see the first lines of lemma, definition, etc commands, which may or may not contain useful information. In the worst case, you just see "lemma" or "definition". It is even worse if you look under a lemma command. This looks like: +lemma |- using |- case |- proof |- apply |- apply |- done |- qed i.e., almost completely useless information.

The enumeration of the commands as "sections" is indeed a bit pointless.

The information that might be useful, i.e. the name and the propositionof the lemma, is displayed nowhere!

Makarius

**Follow-Ups**:**Re: [isabelle] 2014-RC1 issues***From:*Peter Lammich

**References**:**[isabelle] 2014-RC1 issues***From:*Peter Lammich

**Re: [isabelle] 2014-RC1 issues***From:*Peter Lammich

- Previous by Date: Re: [isabelle] 2014-RC1 issues
- Next by Date: Re: [isabelle] check phases
- Previous by Thread: Re: [isabelle] 2014-RC1 issues
- Next by Thread: Re: [isabelle] 2014-RC1 issues
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list