src/Pure/General/buffer.ML
changeset 36237 86e62a98deea
parent 29323 868634981a32
child 60982 67e389f67073
equal deleted inserted replaced
36236:5563c717638a 36237:86e62a98deea