src/Pure/PIDE/resources.ML
changeset 77029 1046a69fabaa
parent 77028 f5896dea6fce
child 77723 b761c91c2447
equal deleted inserted replaced
77028:f5896dea6fce 77029:1046a69fabaa