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

[Mikaël Mayer]

Awesome ! I didn't know there were a graph representation. That's
quasi-exactly what I was looking for.
Thanks for the tips, and have a nice week-end !
Mikaël


2009/10/2 Makarius <makarius at sketis.net>

> 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
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091002/bcf7fa13/attachment.html>