Re: [isabelle] Concrete syntax and default structure



Dear Peter,

records are not flexible enough to achieve what you want since they don't provide multiple inheritance on structures. Your "dirty hack" is a way of simulating this. (My formalisation of additive groups in HOL-Algebra uses an extension of the record for multiplicative groups and ignores the unnecessary fields, so that's quite similar.)

An alternative would be not to use structural parameters and records, but make each of the operations (that is, record entries) a separate parameter. Renaming and syntax annotations in locale expressions then give you full control over the syntax.

Clemens





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