src/Pure/General/symbol_pos.ML
changeset 58839 ccda99401bc8
parent 58047 9f3826352b52
child 58850 1bb0ad7827b4