src/Pure/General/ROOT.ML
changeset 26069 321c4ca82923
parent 25728 71e33d95ac55
child 26077 1498f0362362