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