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

Larry

On 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


Attachment: 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

Reply via email to