Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer



On 16.02.21 08:26, Mathias Fleury wrote:
> 
> Sadly, this is an example that I cannot fix. Sledgehammer has some
> expectations on Skolemization steps that are not true for the proof
> format of veriT, leading to such weird bugs. Many proofs can be fitted
> to fit the expectations, but others cannot easily -- and that one cannot.
> 
> 
> If this is a big issue for you, the solution is to remove veriT from the
> provers used by Sledgehammer.

Thank you for looking into it: for me the main conclusion is that I
don't have to worry about it for the final Isabelle2021 release (to
appear towards the end of the week).


	Makarius





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