src/Pure/General/position.ML
changeset 70610 d14ddb1df52c
parent 70498 de75eea6ffc8
child 71465 910a081cca74
equal deleted inserted replaced
70609:5549e686d6ac 70610:d14ddb1df52c