Re: [isabelle] Simplifier: List of actually used theorems
On 10.07.2013 13:10, Steffen Juilf Smolka wrote:
I think I have seen this question on the mailinglist before, but couldn't find it.
Is there a way to have the simplifier output the subset of supplied facts that were actually used?
Not directly, no. You can extract the theroems used in the proof of a
theorem. The "thm_deps" command gives you a graph of dependencies. Lukas
Bulwahn and Rafal Kolanski once wrote some ML function to print the
direct dependencies of a theorem. I think it ended up in the Isabelle
Cookbook, because there was no consensus how a user-interface to this
functionality should look like.
This archive was generated by a fusion of
Pipermail (Mailman edition) and