src/Pure/General/table.ML
changeset 5526 e7617b57a3e6
parent 5015 44fd9e09c637
child 5681 464913c6086a
equal deleted inserted replaced
5525:896f8234b864 5526:e7617b57a3e6