Re: [isabelle] RC5: Short experience report


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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.