[isabelle-dev] Explicit behaviour of apply(auto) ?

[Makarius]

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