src/Tools/misc_legacy.ML
changeset 42266 f87e0be80a3f
parent 39288 f1ae2493d93f
child 42284 326f57825e1a
equal deleted inserted replaced
42265:ffdaa07cf6cf 42266:f87e0be80a3f