src/HOL/subset.ML
changeset 11908 82f68fd05094
parent 11603 c3724decadef
child 11979 0a3dace545c5