src/Pure/table.ML
changeset 4498 a088ec3e4f5e
parent 4485 697972696f71