src/Pure/General/position.ML
changeset 32626 a45e8ec2b51e
parent 32573 62b5b538408d
child 33097 9d501e11084a
equal deleted inserted replaced
32625:f270520df7de 32626:a45e8ec2b51e