src/Pure/General/position.ML
changeset 13510 0a0f37f9c031
parent 8806 a202293db3f6
child 14981 e73f8140af78
equal deleted inserted replaced
13509:6f168374652a 13510:0a0f37f9c031