src/Pure/ROOT.ML
changeset 52244 cb15da7bd550
parent 52211 66bc827e37f8
child 52470 dedd7952a62c