src/Pure/context_position.ML
changeset 45666 d83797ef0d2d
parent 44736 c2a3f1c84179
child 46874 993c413746f4
equal deleted inserted replaced
45665:129db1416717 45666:d83797ef0d2d