[isabelle] thm_deps



Hi, I'm trying to see what lemmas end up being used by auto in an Isabelle proof. Here's what I did:

  ML {* ThmDeps.enable () *}
  lemma test: "(x::int) * 0 + y = y"
  by auto

  thm_deps test

However, as far as I can see the lemmas auto used to simplify away the occurrences of addition and multiplication don't show up in the graph browser.

Also, is there an existing ML function that, given a theorem proved while theorem dependencies was turned on (i.e. ML {* proofs := 1 *}), would return the list of lemmas used in the proof, or will I have to write something that traverses the theorem's proof object?

Thanks,
-john







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