src/Tools/misc_legacy.ML
changeset 38693 a99fc8d1da80
parent 37781 2fbbf0a48cef
child 39288 f1ae2493d93f
equal deleted inserted replaced
38692:89d3550d8e16 38693:a99fc8d1da80