src/Tools/misc_legacy.ML
changeset 62908 d7009a515733
parent 61914 16bfe0a6702d
child 64548 8b187a7a9776
equal deleted inserted replaced
62907:9ad0bac25a84 62908:d7009a515733