src/Pure/General/buffer.ML
changeset 22534 bd4b954e85ee
parent 21630 d1ca26a2b918
child 23226 441f8a0bd766
equal deleted inserted replaced
22533:62c76754da32 22534:bd4b954e85ee