<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><br>
<div><br><blockquote type="cite"><div>On 25. Jul 2024, at 00:04, Lawrence Paulson <lp15@cam.ac.uk> wrote:</div><br class="Apple-interchange-newline"><div><div>So now the call to <br><br><blockquote type="cite">install_C_file "word_abs.c"<br>autocorres<br> [ (* signed_word_abs is implicit; these are the functions that would be abstracted: *)<br> (*signed_word_abs =<br> S_add_S S_sub_S S_mul_S S_div_S S_mod_S neg_S<br>... , ts_rules = nondet<br>] “word_abs.c”<br></blockquote><br>in AutoCorres2/tests/examples/WordAbs.thy turns purple and hangs, apparently without doing any work.<br><br>Larry<br><br></div></div></blockquote><br></div><div>The Ramsey commit in Isabelle broke that proof. See here.</div><div><br></div><div></div><div>changeset: 14717:a4c2d293808e</div><div>tag: tip</div><div>user: Norbert Schirmer <nschirmer@apple.com></div><div>date: Thu Jul 25 09:37:11 2024 +0200</div><div>summary: fix proof following Isabelle/e65eed943bee</div><div><br></div><div>Regards,</div><div><div>Norbert</div><div><br></div><div>--</div><div><br></div><div>Norbert Schirmer (nschirmer@apple.com)</div><div> SEG Formal Verification</div><div><br></div><br class="Apple-interchange-newline"></div><br class="Apple-interchange-newline" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><div><br></div><div><br></div><div><br></div></body></html>