[isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/1bd81dc4/attachment.bin>