src/Pure/General/buffer.ML
changeset 55986 61b0021ed674
parent 29323 868634981a32
child 60982 67e389f67073
equal deleted inserted replaced
55985:594afef0dd89 55986:61b0021ed674