<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><font size="+1">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.</font><br>
</p>
<br>
<div class="moz-cite-prefix">On 2018-01-18 15:29, Tobias Nipkow
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:6736befe-46f3-c1ca-d721-86a990e7be7c@in.tum.de">So what
is the situation wrt the theories I asked about?
<br>
<br>
Tobias
<br>
<br>
On 18/01/2018 15:11, Lawrence Paulson wrote:
<br>
<blockquote type="cite">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.
<br>
<br>
Larry
<br>
<br>
<blockquote type="cite">On 18 Jan 2018, at 13:31, Tobias Nipkow
<a class="moz-txt-link-rfc2396E" href="mailto:nipkow@in.tum.de"><nipkow@in.tum.de></a> wrote:
<br>
<br>
It sounds like a reasonable criterion. Can you tell us what
that means for Hausdorff_Distance, Metric_Completion and
Isometries (as detailed by Fabian)?
<br>
</blockquote>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>