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.

Larry Paulson


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)?
> 
> cheers
> 
> chris
> 






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