<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>