[isabelle-dev] Gromov Hyperbolicity

[Lawrence Paulson]

We certainly need to solve this problem. One possible criterion: which results are part of a standard undergraduate  athematics curriculum?
Larry

> On 18 Jan 2018, at 10:06, Fabian Immler <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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/446908c2/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/446908c2/attachment.sig>