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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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