src/Pure/General/history.ML
changeset 5526 e7617b57a3e6
parent 5039 28c18f9e106e
child 6680 7f97bb4f790d