src/Pure/General/ROOT.ML
changeset 27094 2cf13a72e170
parent 26880 ebcd5c23dd96
child 27586 b3b6c581c3f9