src/Pure/ROOT.ML
changeset 26288 89b9f7c18631
parent 26279 e8440c90c474
child 26629 6e93fbd4c96a
equal deleted inserted replaced
26287:df8e5362cff9 26288:89b9f7c18631