<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Hi Larry,
<div class=""><br class="">
</div>
<div class="">Just undoing the changes should be easy via "hg backout -r <revision>" for each of the commits in question (going backwards in time).
<div class=""><br class="">
</div>
<div class="">Cheers,</div>
<div class="">Dmitriy<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 21 Aug 2020, at 11:59, Klein, Gerwin (Data61, Kensington NSW) <<a href="mailto:Gerwin.Klein@data61.csiro.au" class="">Gerwin.Klein@data61.csiro.au</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">I’m
happy with either direction as long as we get into a consistent state. If we revert the definition, we’ll also have to revert the AFP fixes, but I’m assuming that this is going to be easier than the other direction.</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">Cheers,</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">Gerwin</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<blockquote type="cite" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
On 21 Aug 2020, at 17:55, Lawrence Paulson <<a href="mailto:lp15@cam.ac.uk" class="">lp15@cam.ac.uk</a>> wrote:<br class="">
<br class="">
Before wasting another week, which incidentally I really can’t spare, it would be nice to know whether there are any objections to going back to the original definition?<br class="">
<br class="">
Larry<br class="">
<br class="">
<blockquote type="cite" class="">On 21 Aug 2020, at 09:34, Lawrence Paulson <<a href="mailto:lp15@cam.ac.uk" class="">lp15@cam.ac.uk</a>> wrote:<br class="">
<br class="">
It’s obvious that this proposal should have been discussed more widely. And I shouldn’t have volunteered to implement it before securing firm offers of help, because it was obvious from the outset that it would be seriously laborious. With this change, a repair
is never as simple as inserting some tactic or rewrite but requires at least a lemma or two. In some cases it’s a problem-solving task taking hours. So I’m sorry it’s taken me so long to reduce 60 failing entries to 20 (and I have fixes to five more in the
pipeline). But I’d be happy to wash my hands of the whole thing.<br class="">
</blockquote>
<br class="">
_______________________________________________<br class="">
isabelle-dev mailing list<br class="">
<a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">
<a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman46.in.tum.de%2Fmailman%2Flistinfo%2Fisabelle-dev&data=02%7C01%7Ctraytel%40di.ku.dk%7C3e7d857e667b4f14b15f08d845b8e924%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637336008072177688&sdata=cjpY6bAE0N6qIyxAz3IkhBKVvJ1vC%2BGwi%2FjIfPZdsnU%3D&reserved=0" class="">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman46.in.tum.de%2Fmailman%2Flistinfo%2Fisabelle-dev&data=02%7C01%7Ctraytel%40di.ku.dk%7C3e7d857e667b4f14b15f08d845b8e924%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637336008072177688&sdata=cjpY6bAE0N6qIyxAz3IkhBKVvJ1vC%2BGwi%2FjIfPZdsnU%3D&reserved=0</a><br class="">
</blockquote>
<br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">_______________________________________________</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">isabelle-dev
mailing list</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<a href="mailto:isabelle-dev@in.tum.de" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">isabelle-dev@in.tum.de</a><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">
<a href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman46.in.tum.de%2Fmailman%2Flistinfo%2Fisabelle-dev&data=02%7C01%7Ctraytel%40di.ku.dk%7C3e7d857e667b4f14b15f08d845b8e924%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637336008072177688&sdata=cjpY6bAE0N6qIyxAz3IkhBKVvJ1vC%2BGwi%2FjIfPZdsnU%3D&reserved=0" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman46.in.tum.de%2Fmailman%2Flistinfo%2Fisabelle-dev&data=02%7C01%7Ctraytel%40di.ku.dk%7C3e7d857e667b4f14b15f08d845b8e924%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637336008072177688&sdata=cjpY6bAE0N6qIyxAz3IkhBKVvJ1vC%2BGwi%2FjIfPZdsnU%3D&reserved=0</a></div>
</blockquote>
</div>
<br class="">
</div>
</div>
</body>
</html>