HomeIsabelle/Phabricator

tuned proofs --- avoid z3, which is absent on arm64-linux;