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



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]

Cheers,

Bertram




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