src/Pure/ROOT.ML
changeset 27179 8f29fed3dc9a
parent 26629 6e93fbd4c96a
child 27254 0f8106808e66
equal deleted inserted replaced
27178:c8ddb3000743 27179:8f29fed3dc9a