I for one have not encountered any of these things in my undergraduate mathematics lectures. But the situation may well be different in other universities.
On 2018-01-18 15:29, Tobias Nipkow wrote: > So what is the situation wrt the theories I asked about? > > Tobias > > On 18/01/2018 15:11, Lawrence Paulson wrote: >> 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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
