src/CCL/subset.ML
changeset 1246 706cfddca75c
parent 757 2ca12511676d
child 1459 d12da312eff4
equal deleted inserted replaced
1245:934183dfc786 1246:706cfddca75c