src/Pure/General/ROOT.ML
changeset 24666 9885a86f14a8
parent 24633 0a3a02066244
child 25715 3d1d281b2471