Re: [isabelle] unused_thms in proofs



Hi Andreas,

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

For Sledgehammer (esp. MaSh), we had to do some fishing around in the local context to retrieve facts in Isar proofs. I am under the impression that all the information we would need is stored in some form.

Jasmin





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