Re: [isabelle] Isabelle2013-RC2 available for testing



On Wed, 6 Feb 2013, Yannick wrote:

On Wed, 06 Feb 2013 20:09:32 +0100, Makarius <makarius at sketis.net> wrote:

On Wed, 6 Feb 2013, Yannick wrote:

I've checked again, that's really “print_rules”. It's suggested by the
completion box which appears when you type “print_” in jEdit and an Isabelle
file is opened. This “print_rules” is one of the most useful to me

How do you use it?

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.

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

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


	Makarius


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