src/Pure/General/output.ML
changeset 32626 a45e8ec2b51e
parent 31685 c124445a4b61
child 32738 15bb09ca0378