src/Pure/General/table.ML
changeset 79946 05e034a54924
parent 79249 718798653cf1
child 80240 534c5e4f07c0
equal deleted inserted replaced
79945:ca004ccf2352 79946:05e034a54924