src/Pure/General/output.ML
changeset 38823 828e68441a2f
parent 38236 d8c7be27e01d
child 38836 52cee2c5f219