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



Bertram Felgenhauer via Cl-isabelle-users wrote:
> Makarius wrote:
> 
> One of the big changes concerns multisets. In the multiset
> extension theory, there is a cancellation law
> (X + Z <ms Y + Z implies X <ms Y), but no corresponding variant
> for add_mset. Is it too late add this? It would be:
> 
> 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)

Cheers,

Bertram





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