src/Pure/General/buffer.ML
changeset 25955 94a515ed8a39
parent 23785 ea7c2ee8a47a
child 26502 7f64d8cf6707
equal deleted inserted replaced
25954:682e84b60e5c 25955:94a515ed8a39