src/Pure/ROOT.ML
changeset 38777 a94559e26000
parent 38634 bff9c05fe229
child 38874 4a4d34d2f97b