Email Gateway (Aug 19 2022 at 11:29): Email Gateway (Aug 19 2022 at 11:29):From: Steffen Juilf Smolka <steffen.smolka@in.tum.de>
Hi,
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?
Regards,
Steffen
Email Gateway (Aug 19 2022 at 11:29):From: Lars Noschinski <noschinl@in.tum.de>
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
Last updated: Apr 25 2024 at 01:08 UTC