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.

Cheers,
	Florian Haftmann

-- 

PGP available:
http://isabelle.in.tum.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.