src/HOL/Induct/Multiset0.thy
changeset 8490 6e0f23304061
parent 5628 15b7f12ad919
equal deleted inserted replaced
8489:bb41d88f7df5 8490:6e0f23304061