src/Pure/General/output.ML
changeset 16081 81a4b4a245b0
parent 15531 08c8dad8e399
child 16191 9d503d6fcbb1