Jasmin, Greatr work! On 15/02/2021 10:16, Jasmin Blanchette via Cl-isabelle-users wrote:
2. Sledgehammer now includes the Zipperposition higher-order prover that's developed largely by my team. It won last year CASC's higher-order division by a record margin. It's not enabled by default because we ran out of time to test it thoroughly, but you can add it to the Sledgehammer panel or "sledgehammer_params".
How exactly do you activate Zipperposition? Tobias
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature