Re: [isabelle] HOL/List.thy lemma suggestions

I had been afraid that if I add these lemmas I would open the floodgates for many similar generalizations. But having looked at the existing lemmas, I found that this fear was unjustified and I added them:


On 18/05/2018 17:34, Lukas Bulwahn wrote:
On Fri, May 18, 2018 at 4:41 PM, Tobias Nipkow <nipkow at> wrote:
Hi Lukas,

Your lemmas look natural but replacing the existing simp-rules with them
broke a number of proofs and didn't help any. Thus I have left things as
they are. I didn't add them as ordinary lemmas because my impression is that
in most cases one zips lists of the same length.

Too bad.

Is there a chance to put the two lemmas (without simp attribute) in
the More_List theory in HOL-Library?

That might be an acceptable compromise for everyone.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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