src/Pure/General/buffer.ML
changeset 16809 8ca51a846576
parent 16712 c7d1c79d921c
child 17062 7272b45099c7