src/Pure/table.ML
changeset 4617 cea2a5b5ee10
parent 4485 697972696f71
equal deleted inserted replaced
4616:d257e6c6614f 4617:cea2a5b5ee10