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



On Fri, May 18, 2018 at 4:41 PM, Tobias Nipkow <nipkow at in.tum.de> 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.

Lukas




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