src/Pure/General/position.ML
changeset 78546 e3ae7293c5df
parent 78023 76dece8cd8a7
child 78811 d3328c562307