src/Pure/context_position.ML
changeset 71986 76193dd4aec8
parent 71680 e20e117c3735
child 76804 3e8340fcaa16
equal deleted inserted replaced
71985:a1cf296a7786 71986:76193dd4aec8