HomeIsabelle/Phabricator

tuned proofs: avoid z3 to make it work on arm64-linux;