src/Pure/General/symbol_pos.ML
changeset 55672 5e25cc741ab9
parent 55107 1a29ea173bf9
child 55709 4e5a83a46ded