src/Pure/General/history.ML
changeset 20664 ffbc5a57191a
parent 16496 8144814dc6a1
child 21175 98c0405f5493
equal deleted inserted replaced
20663:2024d9f7df9c 20664:ffbc5a57191a