src/Pure/General/table.ML
changeset 5526 e7617b57a3e6
parent 5015 44fd9e09c637
child 5681 464913c6086a