<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">Okay it is done now </div>
</div>
<div name="messageSignatureSection"><br>
<div class="matchFont">
<div dir="auto">Larry</div>
</div>
</div>
<div name="messageReplySection">On 25 Jan 2024 at 21:09 +0000, Fabian Immler <fabian.immler@gmail.com>, wrote:<br>
<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">
<div dir="auto">Hi Achim,</div>
<div dir="auto"><br>
</div>
<div dir="auto">Thank you for these suggestions. From my point of view (as one of the authors of <span style="float:none;display:inline!important;background-color:rgba(0,0,0,0);border-color:rgb(0,0,0);color:rgb(0,0,0)">HOL-Library.Interval</span>), these changes
are reasonable and could go to the Isabelle distribution (after testing with the AFP).</div>
<div dir="auto">Unfortunately I currently don’t have access to the development repository.</div>
<div dir="auto"><br>
</div>
<div dir="auto">Would somebody reading this volunteer to bring these changes to isabelle-dev?</div>
<div dir="auto"><br>
</div>
<div dir="auto">Best wishes,</div>
<div dir="auto">Fabian</div>
<div dir="auto"><br>
</div>
<div dir="auto"><br>
</div>
<div><br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Jan 22, 2024 at 11:34 Achim D. Brucker <<a href="mailto:adbrucker@0x5f.org">adbrucker@0x5f.org</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)">
<br>
Hi,<br>
In the theory HOL-Library.Interval, the type "'a interval" uses the<br>
following instantiation for the type class "times":<br>
<br>
instantiation "interval" :: (linordered_semiring) times<br>
<br>
This prevents, for instance, using interval multiplication with the<br>
instance "ereal interval".<br>
<br>
It seems to be possible to "relax" the instantiation for<br>
times/multiplication-related type classes to "{times, linorder}",<br>
which is supported by ereal (and, hence, allows for using interval<br>
multiplication over extended reals).<br>
<br>
I did locally change the instantiations in HOL-Library.Interval and<br>
rebuilt HOL-Library without any problems. HOL-Library.Interval is not<br>
used a lot. Still, given that this change makes the interval type<br>
applicable in more situation, I do not expect any major problems with<br>
this change.<br>
<br>
My changes are described in the attached patch (relative to the<br>
Isabelle development tip 79579:57ceacd4a17b).<br>
<br>
Is this a change that could make it into the Isabelle distribution?<br>
<br>
<br>
Best,<br>
Achim</blockquote>
</div>
</div>
</blockquote>
</div>
</body>
</html>