src/Pure/General/buffer.ML
changeset 27390 49a54b060457
parent 26545 6e1aef001b3b
child 28027 051d5ccbafc5
equal deleted inserted replaced
27389:823c7ec3ea4f 27390:49a54b060457