[isabelle-dev] New Sledgehammer multitheading model

Tobias Nipkow nipkow at in.tum.de
Tue Feb 1 16:48:16 CET 2022


Hi Jasmin,

I'm looking forward to trying the new model.

On 01/02/2022 09:39, Jasmin Blanchette wrote:
> Apart from that, the main visible difference is that you may now see several proofs coming from the same prover,

That is because you invoke the same prover with different parameters?

Tobias
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220201/17060504/attachment.bin>


More information about the isabelle-dev mailing list