src/Pure/context_position.ML
changeset 48370 d0fa3efec93b
parent 47813 18de60b8c906
child 48767 7f0c469cc796
equal deleted inserted replaced
48369:10b534e64209 48370:d0fa3efec93b