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.

  -- Lars




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