src/Pure/General/symbol_pos.ML
changeset 27885 76b51cd0a37c
parent 27864 827730aea9e8
child 27984 b4dd58cff97c