On 29/04/2016 10:39, Andreas Lochbihler wrote:
Dear all, I have written several Isar-style proofs of lemmas each of which is quite long (>1000 lines). As the proofs have evolved over time, I am not sure any more that I use every intermediate result to prove the result. Is there any convenient way to find out whether there are some unused intermediate steps? I tried to use unused_thms before the final qed, but this gives me only top-level theorems, not intermediate (named) facts stated with "have". I could imagine a diagnostic command that one issues before the qed and it lists all the unused intermediate facts since the last "next" or "proof" command on the same level. If this is not available, could this be implemented and how hard would it be? Would anyone else find such a functionality useful?
I would. Especially if it is integrated with the interface and marks such unused local facts (on demand).
Description: S/MIME Cryptographic Signature