src/Pure/table.ML
changeset 5014 32e6cab5e7d4
parent 4485 697972696f71