src/Pure/General/ROOT.ML
changeset 5526 e7617b57a3e6
parent 5040 78abd4c4802a
child 5864 30b6a3251813