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"?
Description: OpenPGP digital signature