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.

Cheers,
René

(IsaFoR/CeTA can be accessed at http://cl-informatik.uibk.ac.at/software/ceta/)



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