src/Pure/General/history.ML
changeset 5253 82a5ca6290aa
parent 5039 28c18f9e106e
child 6680 7f97bb4f790d