subset.thy
changeset 119 93dc86ccee28
parent 116 ab4328bbff70