[isabelle-dev] Gromov Hyperbolicity
nipkow at in.tum.de
Thu Jan 18 14:31:47 CET 2018
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
> 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)?
>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev