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 <nip...@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)? _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
