rename EVERY2 to LIST_REL in theorem names

[xrchz]

EVERY2 and LIST_REL are the same constant (one is an overload for the other). But several theorems use "EVERY2" in their name, which makes it hard to find theorems about "LIST_REL" if one only knows the constant by that name. It would be nice if all the theorems used "LIST_REL" in their name. (Suggested by @SOwens.)

---

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[konrad-slind]

This is a general problem. If existing constants are going to be renamed/overloaded, then perhaps the search facilities should look at the overloading maps in order to get all the info.

Konrad.

On Wed, Nov 11, 2015 at 11:05 AM, Ramana Kumar [email protected] wrote:

EVERY2 and LIST_REL are the same constant (one is an overload for the other). But several theorems use "EVERY2" in their name, which makes it hard to find theorems about "LIST_REL" if one only knows the constant by that name. It would be nice if all the theorems used "LIST_REL" in their name. (Suggested by @SOwens https://github.com/SOwens.)

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/316.

[mn200]

If you want to add additional bindings so that theorems are available under two names, that's fine. On the other hand, don't remove existing bindings to break stuff gratuitously.

I'd tend to use DB.match in preference to DB.find, and then the name of the theorem doesn't really matter.

[xrchz]

#319 is relevant

[xrchz]

#98 also