src/Pure/General/change_table.ML
changeset 77852 df35b5b7b6a4
parent 77723 b761c91c2447
child 77974 93999ffdb9dd