Re: [isabelle] Isabelle2014-RC0: add_assoc hidden, causes error, but proof passes

Hi Gottfried,

> There's "Groups.semigroup_add.add_assoc", followed in Groups.thy by
> "hide_fact add_assoc". The "hide_fact" is new in Groups.thy and causes
> an error in a proof.

this is a misunderstanding.  The canonical name for associativity of
plus is now add.assoc, cf. NEWS.

The add_assoc you have stumbled over is just a device to bootstrap the
locale / type class hierarchy.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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