src/HOL/Library/Multiset.thy
changeset 80898 71756d95b7df
parent 80786 70076ba563d2
child 80914 d97fdabd9e2b
equal deleted inserted replaced
80897:5328d67ec647 80898:71756d95b7df