So what is the situation wrt the theories I asked about?


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.


On 18 Jan 2018, at 13:31, Tobias Nipkow <> 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)?

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to