src/HOL/subset.thy
changeset 7990 0a604b2fc2b1
parent 7717 e7ecfa617443
child 9895 75e55370b1ae