src/Pure/General/buffer.ML
changeset 7535 599d3414b51d
parent 6316 4a786a8a1a97
child 7754 4b1bc1266c8c
equal deleted inserted replaced
7534:30344dde83ab 7535:599d3414b51d