changelog.txt currently lists removed Definitions / Lemmas / etc. but not what to use instead, making the user stuck at upgrading their scripts dependent on the removed things.
This draft PR is an attempt to add comments to previously removed items.
I am not sure how thoroughly this should be done, thus just a draft.
changelog.txtcurrently lists removed Definitions / Lemmas / etc. but not what to use instead, making the user stuck at upgrading their scripts dependent on the removed things.This draft PR is an attempt to add comments to previously removed items. I am not sure how thoroughly this should be done, thus just a draft.