src/Pure/General/buffer.ML
changeset 23644 e28b8e8a85b6
parent 23226 441f8a0bd766
child 23785 ea7c2ee8a47a
equal deleted inserted replaced
23643:32ee4111d1bc 23644:e28b8e8a85b6