src/Pure/General/position.ML
changeset 37724 6607ccf77946
parent 37533 d775bd70f571
child 38236 d8c7be27e01d
equal deleted inserted replaced
37723:831b3eb7ed8e 37724:6607ccf77946