src/Pure/Thy/document_output.ML
changeset 73983 e2913fc81142
parent 73780 466fae6bf22e
child 74373 6e4093927dbb