On 18/01/2018 12:48, Lawrence Paulson wrote:
We certainly need to solve this problem.
Absolutely. For practical reasons I would put as much in the AFP as possible, (One could make exceptions for small theories, but this could get out of hand again).
One possible criterion: which results are part of a standard undergraduate athematics curriculum?
It sounds like a reasonable criterion. Can you tell us what that means for Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?
Tobias
LarryOn 18 Jan 2018, at 10:06, Fabian Immler <imm...@in.tum.de <mailto:imm...@in.tum.de>> wrote:We do not have a precise specification of what HOL-Analysis is or should be. I think that makes it very hard to draw a line between material that should go to HOL-Analysis and what should remain in the AFP. So take this as just my personal view._______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
