[isabelle] attribute: rule_format

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 MHonArc.