Re: [isabelle] simp warnings for cong rules

On Mon, 11 May 2015, Lars Noschinski wrote:

There is also the thing that "cong del" lies about its (moral) signature: it deletes not the specified congruence rule, but the congruence rule for the given constant (which is determined from the congruence rule).

That is an important observation: rules are both indexed and *identified* by the head constant here.

Normally the index is just a data structure to help retrieval, while the identity of rules works via Thm.eq_thm_prop. This would allow multiple rules to be declared, and the latest addition for a particular constant is used, the are others ignored. After deletion of some rules, ignored ones might come back in front.

I've put this on the list of things to be reformed for a future release, unless someone points out why this odd historical behaviour has to remain like that.


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