src/Pure/General/output.ML
changeset 51587 7050c4656fd8
parent 50505 33c92722cc3d
child 51661 92e58b76dbb1