src/Pure/General/buffer.ML
changeset 23390 01ef1135de73
parent 23226 441f8a0bd766
child 23785 ea7c2ee8a47a
equal deleted inserted replaced
23389:aaca6a8e5414 23390:01ef1135de73