src/HOL/subset.thy
changeset 6330 e1faf0f6f2b8
parent 5853 36b5559d8224
child 7705 222b715b5d24