src/Tools/misc_legacy.ML
changeset 61639 6ef461bee3fa
parent 60642 48dd1cefb4ae
child 61914 16bfe0a6702d
equal deleted inserted replaced
61638:7ffc9c4f1f74 61639:6ef461bee3fa