src/Pure/General/symbol_pos.ML
changeset 55824 22bc50a19afa
parent 55709 4e5a83a46ded
child 55828 42ac3cfb89f6