src/Pure/General/ROOT.ML
changeset 26436 dfd6947ab5c2
parent 26097 943582a2d1e2
child 26523 18ccad3ecb2e