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


<head>


<meta http-equiv="Content-Type" content="text/html; charset=utf-8">


<title></title>


</head>


<body>


<div name="messageBodySection">


<div dir="auto">I agree with Tobias. We are already very good at preserving our past, but it’s exasperating when novices stumble across legacy material and emulate that style. Fortunately, there is not a single use of BigO anywhere in the AFP. Let’s delete


 it altogether.</div>


</div>


<div name="messageSignatureSection"><br>


<div class="matchFont">


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


</div>


</div>


<div name="messageReplySection">On 11 Jan 2023 at 08:06 +0000, Tobias Nipkow <nipkow@in.tum.de>, wrote:<br>


<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">


<br>


<div>The distribution is meant to provide a curated set of theories. They are in<br>


constant flux anyway. And if some theory is definitely outdated we should remove<br>


it rather than keep it around and confuse users. For archeological purposes we<br>


have mercurial.</div>


</blockquote>


</div>


</body>


</html>