
<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 think it should be deleted. It’s confusing to have two copies of the same material, and I even wasted time trying to move the preliminaries out of there; perhaps they should be deleted as well.</div>


</div>


<div name="messageSignatureSection"><br>


<div class="matchFont">


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


</div>


</div>


<div name="messageReplySection">On 15 Aug 2022, 14:54 +0100, Manuel Eberl <manuel@pruvisto.org>, 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>As for why I did not delete the version in HOL-ex, I cannot remember –<br>


perhaps because it still is a small and self-contained derivation of<br>


that result.</div>


</blockquote>


</div>


</body>


</html>