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

Dear Benedikt,

> 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.

They are also used in the archive of formal proofs and in IsaFoR/CeTA, e.g., in the Matrix entry of the AFP and in Linear_Poly...
within IsaFoR.

Perhaps these examples will be help.


(IsaFoR/CeTA can be accessed at

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