Re: [isabelle] Isabelle2016-1-RC3 available for testing

Dear Bertram,

>> lemmas mult_cancel1 = mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right]
> Sorry, it should be
> lemmas mult_cancel1 = mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right empty_neutral]
> (I had used `simplified`, and didn't spot the lingering empty multiset)

I guess we could add it. However, to what extent is this a critical issue that needs to be resolved before the release, as opposed to after? I believe that IsaFoR already contains a theory file full with multiset lemmas. My suggestion would be for you to add it there, and for us (the Isabelle developers), to add it in the development version of Isabelle (i.e. for Isabelle2017). Unless it is more critical than it looks like.

(Getting closer to a release, it makes sense to become more and more conservative in the changes we incorporate. Otherwise, we'll never converge.)



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