[isabelle] [Sledgehammer]


I found a problem with the usage of sledgehammer's proposed solutions:
sometimes, even if it states "Proof found" and it manages to output an
one-line proof without the "timed-out" assertion, the proposed solution
does not work. This problem arrives to me with a certain frequency. Today,
for example, It happened two times in the same proof.

I am available to help solving this problem.


Paulo Emílio de Vilhena.

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