Re: [isabelle] (structure) and \<index>

On 30.10.2013 11:07, bnord wrote:
> Hi all,
> I was looking into the Isabelle HOL/Algebra library, as I've a student
> who wants to do similar stuff (maybe on top of this).
> I am little bit confused about the (structure) keyword and the related
> \<index>. They only seem to be used in this Library and the Isar
> reference is rather brief about them also, the locales tutorial doesn't
> mention them at all.
> I have two questions about this:
> 1. What is the precise semantics of these constructs? Is there some
> documentation I've missed? The isar reference only mentions that it is
> used for some kind of implicit references.

When you are inside a context where some value is marked as (structure),
this value is used to fill in the argument marked with \<index>.

If you are not inside such a context (or you want to override the
argument), you use \<bsub>..\<esub>.

> 2. Assuming their use is still advised and appropriate for this setting:
> They still seem work only using the \<bsub>..\<esub> syntax which is
> broken in the JEdit interface, is there a way to move away from this?

What do you mean by "broken"?

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.