src/Pure/General/ROOT.ML
changeset 26637 0bfccafc52eb
parent 26523 18ccad3ecb2e
child 26880 ebcd5c23dd96