src/Pure/General/buffer.ML
changeset 82282 919eb0e67930
parent 80822 4f54a509bc89
equal deleted inserted replaced
82281:9357ef19fc56 82282:919eb0e67930