src/HOL/subset.thy
changeset 3225 cee363fc07d7
parent 1475 7f5a4cd08209
child 5853 36b5559d8224