src/Tools/misc_legacy.ML
changeset 51750 cb154917a496
parent 51429 48eb29821bd9
child 52223 5bb6ae8acb87
equal deleted inserted replaced
51749:c27bb7994bd3 51750:cb154917a496