Re: [isabelle] Isabelle Foundation & Certification
Sledgehammer is also useful here, because generally you get to see exactly which facts have been used to prove the theorem. Sometimes you may see a fact being used there doesnât appear to be relevant. Itâs always worth checking to see what is going on.
> On 17 Sep 2015, at 13:06, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> However, thinking about this problem just now, I realised that something similar to the existing AutoQuickcheck could be helpful: something that says "you seem to be trying to prove this the hard way, but it's actually very simple because your assumptions imply False!".
This archive was generated by a fusion of
Pipermail (Mailman edition) and