# [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.*