src/Pure/General/history.ML
changeset 19343 91c348f05f1a
parent 16496 8144814dc6a1
child 21175 98c0405f5493
equal deleted inserted replaced
19342:094a1c071c8e 19343:91c348f05f1a