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.

Larry

> 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 MHonArc.