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.


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

On 29.04.2016, at 13:00, Christian Sternagel <c.sternagel at> 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.)


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