src/Pure/General/ROOT.ML
changeset 26741 eb15fd4cd1ad
parent 26523 18ccad3ecb2e
child 26880 ebcd5c23dd96