src/Tools/misc_legacy.ML
changeset 43760 ef8375a4dae4
parent 42361 23f352990944
child 44121 44adaa6db327
equal deleted inserted replaced
43759:d93a69672362 43760:ef8375a4dae4