So what is the situation wrt the theories I asked about?
Tobias On 18/01/2018 15:11, Lawrence Paulson wrote:
This is mainly a negative criterion, i.e., something outside the undergraduate curriculum probably should not be in our core libraries. But I would guess for example mathematicians cover Gödel's theorem, which we would not want to move to our core libraries. LarryOn 18 Jan 2018, at 13:31, Tobias Nipkow <nip...@in.tum.de> wrote: It sounds like a reasonable criterion. Can you tell us what that means for Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?
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
