src/Pure/General/table.ML
changeset 69762 58fb0d779583
parent 67557 a965ccf7414e
child 70586 57df8a85317a
equal deleted inserted replaced
69761:a899ca03d74c 69762:58fb0d779583