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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and