Re: [isabelle] Algebraic_Numbers

> I noticed that a huge chunk of the resource hunger of that development
> actually comes from Algebraic_Number_Tests.thy, which one does not even
> need in order to use the development.
> Now, I don't know if and by how much this reduces the memory
> requirements and I have no idea how to measure this reliably. In any
> case, I do not see any drawbacks of doing this.

IMHO it is good style that things on which others are supposed to build
upon contain only libraries, not tests.  So, I would suggest to go ahead.

	Florian Haftmann


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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