src/Pure/Syntax/symbol_font.ML
changeset 4273 c9b577c8f7a1
parent 4144 873489c611fc