Re: [isabelle] attribute: rule_format
I think it was just a little more difficult to implement, and never necessary, because you could always write your original theorem in the form P —> Q —> R rather than P & Q —> R. And this sort of thing was only necessary for proof by induction anyway.
With the Isar induction methods, which had been around for several years now, the rule_format attribute is quite unnecessary. It is retained only so that legacy proofs will continue to work.
On 1 Nov 2012, at 05:24, Christian Sternagel <c-sterna at jaist.ac.jp> wrote:
> What is the reason for "rule_format" not to touch HOL conjunction in premises, i.e., why is, e.g., "A & B --> A" not transformed into "A ==> B ==> A" by "rule_format"?
> I often thought such a behavior useful. Is there another way of replacing every HOL connective by an appropriate Pure connective (as far as possible)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and