[isabelle-dev] Gromov Hyperbolicity

Lawrence Paulson lp15 at cam.ac.uk
Thu Jan 18 15:11:28 CET 2018


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)?




More information about the isabelle-dev mailing list