[isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

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 <immler at in.tum.de 
>> <mailto:immler at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- 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/2647f737/attachment.bin>