On Fri, 2 Oct 2009, Mika?l Mayer wrote:
> I tried prf, but it gave only an "?", when it was outside the proof, and
> failed when it was inside the proof.
You need to enable full recording of proofs first, saying something like
ML_command {* proofs := 2 *} in your theory. (This assumes that
Isabelle/HOL has already been built with full proofs, which is the default
in our official precompiled image.)
> lemma test: "\<forall>x. (P(x) \<and> (\<exists>z. Q(x, z)) \<and>
>> (\<forall>x z. Q(x, z)=Q(f(x), z)))\<longrightarrow> (\<exists>z. Q(f(x),
>> z))"
>> by auto
>> prf test
You can also try this:
thm_deps test
If you open the tree folds of "HOL" you will see a list of theorems -- the
graph view is not so nice in this case.
Makarius
