Re: [isabelle] unused_thms in proofs



Hi Jasmin,

That's a good idea. I don't know whether the current implementation of reasoning actually supports such a command. Makarius might know better. But if it does, I guess that this could be a reasonably-sized project for a student.

Andreas

On 29/04/16 17:18, Jasmin Blanchette wrote:

On 29.04.2016, at 13:00, Christian Sternagel <c.sternagel at gmail.com> wrote:

This would definitely be useful! +1 - chris

A student came to me and asked for a 6-week internship project (starting in August). Perhaps this could be something suitable for him? (But if anybody else wants to implement this, go ahead and don't wait for us.)

Jasmin






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