src/Pure/General/output.ML
changeset 56355 1a9f569b5b7e
parent 56334 6b3739fee456
child 56830 e760242101fc