[isabelle] (structure) and \<index>
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and