<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>No objections in principle, but as always, deleting it may break
existing citations. We could leave it in and replace its content
with just a link to the AFP entry. Or just delete it and not care
about external references. I don't have any strong feelings about
this – perhaps Lukas will comment on this as well.</p>
<p>Manuel</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 15/08/2022 16:41, Lawrence Paulson
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:d3000ecb-3f6c-4799-9268-c6943fe09878@Spark">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title></title>
<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 <a class="moz-txt-link-rfc2396E" href="mailto:manuel@pruvisto.org"><manuel@pruvisto.org></a>, 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>
</blockquote>
</body>
</html>