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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and