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



Jasmin Blanchette wrote:
> 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?

You're right, it's not critical.

Cheers,

Bertram




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