src/Pure/General/output.ML
changeset 17740 fc385ce6187d
parent 17539 b2ce48df4d4c
child 18682 216692feebab