src/Pure/General/buffer.ML
changeset 79114 686b7b14d041
parent 75566 389b193af8ae
child 80822 4f54a509bc89
equal deleted inserted replaced
79113:5109e4b2a292 79114:686b7b14d041