src/Pure/General/buffer.ML
changeset 56939 c2ddbf327bbd
parent 29323 868634981a32
child 60982 67e389f67073
equal deleted inserted replaced
56938:ef44b488bad8 56939:c2ddbf327bbd