src/Tools/misc_legacy.ML
changeset 56381 0556204bc230
parent 56245 84fc7dfa3cd4
child 58950 d07464875dd4
equal deleted inserted replaced
56380:9bb2856cc845 56381:0556204bc230