HomeIsabelle/Phabricator

simplified 'smt_proofs' option to be a binary option (instead of ternary), now…

Description

simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)

Details

Provenance
blanchetteAuthored on
Parents
rISABELLE35a2ac83a262: New Ackermann development
Branches
Unknown
Tags
Unknown