src/Pure/General/output.ML
changeset 73613 c1d8cd6d1a49
parent 71637 45c2b8cf1b26
child 73834 364bac6691de
equal deleted inserted replaced
73612:f28df88c0d00 73613:c1d8cd6d1a49