
<html xmlns="http://www.w3.org/1999/xhtml">

<head>

<title></title>

</head>

<body>

<div name="messageBodySection">

<div dir="auto">Thanks, I’ll see what I can do. Ideally, the old versions should be abbreviations but I won’t attempt that all at once.</div>

</div>

<div name="messageSignatureSection"><br />

<div class="matchFont">

<div dir="auto">Larry</div>

</div>

</div>

<div name="messageReplySection">On 25 Feb 2020, 17:45 +0000, Manuel Eberl <eberlm@in.tum.de>, wrote:<br />

<blockquote type="cite" class="spark_quote" style="margin: 5px 5px; padding-left: 10px; border-left: thin solid #1abc9c;"><br />

<div>Apparently we do, in src/HOL/Analysis/Borel_Space.thy.<br />

<br />

Don't ask me why. Yes, it should be moved.</div>

</blockquote>

</div>

</body>

</html>