src/Pure/Thy/document_output.ML
changeset 73828 201200b549fc
parent 73780 466fae6bf22e
child 74373 6e4093927dbb