[isabelle] (structure) and \<index>



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.

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?

Best
Benedikt




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