Re: [isabelle] Isabelle2013-RC2 available for testing



On Wed, 06 Feb 2013 21:40:33 +0100, Makarius <makarius at sketis.net> wrote:

I use it to know what's the available rules for the “rule” proof method.
This help to to guess what “rule” alone used as much as to give “rule”
an explicit argument.

OK.  In the meantime I have also added its documentation in isar-ref, so
it will be in Isabelle2013-RC3 soon.

I will wait for RC3 and re‑read the isar-ref.pdf file so. Do you know if RC3 “print_rules” will always displays the rules without names? Actually, it helps for the first use case (guess what “rule” use), but not the second (giving “rule” explicit arguments).

Note that method "rule" is dynamically rebound in HOL to include rules
stemming from the classical reasoner, too.  Cf. print_claset.

I'm not sure to understand what it implies, but will learn “print_claset”, as you mention it.

At some point I would like to see proper feedback by the Prover IDE about
these implicit single-step rules applied here.  Next release ...

Wow, great! :) I was wishing this. Before I came to Isabelle, at the time I didn't knew any prover system, I tried to imagine such things, and in my mind, this was always coming with this: “if it automate some proof or proof step, the user should be able to learn what the steps was, it should be visible in some way”. That's important, as the matter, I feel, is not only about the prover understanding a proof, but also about the human author and human reader, understanding it too.

Many thanks for the great point!

--
Yannick Duchêne





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.