
<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">In the AFP, grep picks up these:<div class=""><br class=""></div><div class=""><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./Coinductive/Examples/CCPO_Topology.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./Concurrent_Ref_Alg/Refinement_Lattice.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./DataRefinementIBP/Diagram.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./DataRefinementIBP/Hoare.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./DataRefinementIBP/Statements.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./LatticeProperties/Conj_Disj.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./MonoBoolTranAlgebra/Mono_Bool_Tran.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy</span></div><div style="margin: 0px; line-height: normal; font-family: Consolas; background-color: rgb(209, 253, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">./PSemigroupsConvolution/Quantales.thy</span></div><div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div><div class="">But why would they fail? The new version is surely stronger, so any changes should be pretty straightforward, right? </div><div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div><div class="">

<span class="Apple-style-span" style="border-collapse: separate; font-family: Helvetica; font-size: 11px; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: normal; border-spacing: 0px;"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">Larry</div></div></span>

</div>

<br class=""><div><blockquote type="cite" class=""><div class="">On 27 Aug 2017, at 15:59, Viorel Preoteasa <<a href="mailto:viorel.preoteasa@aalto.fi" class="">viorel.preoteasa@aalto.fi</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="font-family: Consolas; font-size: 13px; 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; float: none; display: inline !important;" class="">There is also AFP. If there are instantiations of complete_distrib_lattice, then most probably they will fail.</span><br style="font-family: Consolas; font-size: 13px; 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;" class=""><br style="font-family: Consolas; font-size: 13px; 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;" class=""><span style="font-family: Consolas; font-size: 13px; 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; float: none; display: inline !important;" class="">One simple solution in this case could be to keep also the</span><br style="font-family: Consolas; font-size: 13px; 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;" class=""><span style="font-family: Consolas; font-size: 13px; 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; float: none; display: inline !important;" class="">old complete_distrib_lattice as complete_pseudo_distrib_lattice.</span><br style="font-family: Consolas; font-size: 13px; 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;" class=""><br style="font-family: Consolas; font-size: 13px; 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;" class=""></div></blockquote></div><br class=""></div></body></html>