Awesome ! I didn't know there were a graph representation. That's quasi-exactly what I was looking for.<br>Thanks for the tips, and have a nice week-end !<br clear="all">Mikaël<br>
<br><br><div class="gmail_quote">2009/10/2 Makarius <span dir="ltr"><<a href="mailto:makarius@sketis.net">makarius@sketis.net</a>></span><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">

<div class="im">On Fri, 2 Oct 2009, Mikaël Mayer wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I tried prf, but it gave only an "?", when it was outside the proof, and failed when it was inside the proof.<br>
</blockquote>
<br></div>
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.)<div class="im">

<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
lemma test: "\<forall>x. (P(x) \<and> (\<exists>z. Q(x, z)) \<and><br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
(\<forall>x z. Q(x, z)=Q(f(x), z)))\<longrightarrow> (\<exists>z. Q(f(x),<br>
z))"<br>
by auto<br>
prf test<br>
</blockquote></blockquote>
<br></div>
You can also try this:<br>
<br>
  thm_deps test<br>
<br>
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.<br><font color="#888888">
<br>
<br>
        Makarius<br>
</font><br>_______________________________________________<br>
Isabelle-dev mailing list<br>
<a href="mailto:Isabelle-dev@mailbroy.informatik.tu-muenchen.de">Isabelle-dev@mailbroy.informatik.tu-muenchen.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br>
<br></blockquote></div><br>