src/Pure/General/ROOT.ML
changeset 5253 82a5ca6290aa
parent 5040 78abd4c4802a
child 5864 30b6a3251813