src/Pure/General/buffer.ML
changeset 47762 d31085f07f60
parent 29323 868634981a32
child 60982 67e389f67073
equal deleted inserted replaced
47761:dfe747e72fa8 47762:d31085f07f60