Re: [isabelle] unused_thms in proofs
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and