
<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">Since we describe that directory as “miscellaneous examples”, anything we put there needs to be presentable, so the theory will require a bit of tidying up.</div>


</div>


<div name="messageSignatureSection"><br>


<div class="matchFont">


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


</div>


</div>


<div name="messageReplySection">On 11 Jan 2023 at 13:08 +0000, Makarius <makarius@sketis.net>, wrote:<br>


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


On 11/01/2023 12:48, Lawrence Paulson wrote:<br>


<blockquote type="cite">That is an entirely different situation. It’s used as test data. Nobody will<br>


get confused or distracted by that.<br>


</blockquote>


<br>


I find it confusing to have a clone with its original lost in time and space.<br>


<br>


If you want to avoid general user confusion, the traditional approach is to<br>


move it into the "HOL-ex" bin.<br>


<br>


<br>


Makarius<br>


<br>


<br>


</blockquote>


</div>


</body>


</html>