src/Pure/General/output.ML
changeset 48133 a5ab5964065f
parent 47999 3ffd885abe00
child 49647 21ae8500d261