I wonder whether some of this material should be moved to the Analysis library. Larry
> 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.
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
