src/Pure/General/output.ML
changeset 80863 af34fcf7215d
parent 80849 e3a419073736