src/Pure/Thy/to_html.ML
changeset 1290 ee8f41456d28
parent 1227 c9f7848bc5ee