[isabelle-dev] Proven support for Linux ARM64

[Lawrence Paulson]

Somewhat to my surprise, there seem to be 1004 occurrences of “smt(z3" in the libraries and repository (I've never allowed it personally). It is outnumbered by verit more than 3 to 1, again a surprisingly low ratio. 

Getting rid of them all would be a tedious business. One day we might consider automated tools to crawl over old the proofs and get rid of ugly things. 

Larry

> On 14 Feb 2024, at 07:47, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de> wrote:
> 
> 1. Replace the "smt" calls. Most of them could use the "(verit)" option instead, and for the others, we'd have to come up with alternative proofs. This possibly entails a lot of work, but it could be done by a "task force".
>