I wonder whether some of this material should be moved to the Analysis library.

> On 18 Jan 2018, at 06:51, Tobias Nipkow <nip...@in.tum.de> wrote:
> Along the way, we introduce basic material on isometries, quasi-isometries, 
> Lipschitz maps, geodesic spaces, the Hausdorff distance, the Cauchy 
> completion of a metric space, and the exponential on extended real numbers.

Attachment: signature.asc
Description: Message signed with OpenPGP

isabelle-dev mailing list

Reply via email to