src/Pure/General/output.ML
changeset 14867 6dd1f25b3d75
parent 14862 a43f9e2c6332
child 14869 544be18288e6