rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert

As discussed this is currently inconsistent.

I propose we use insert_delete for the lemma with a precondition since it is used 7 times in std++ after this MR; the one without a precondition is used just 3 times (one of which is to prove insert_delete).

LGTM modulo nit.

added 1 commit

• 2f6b9769 - changelog

Compare with previous version

resolved all threads

Can you rebase? There's conflicts in the CHANGELOG. Thanks :).

added 5 commits

• 2f6b9769...e3800ea7 - 3 commits from branch master
• 942c669a - rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert
• cffd6689 - changelog

Compare with previous version

done.

@robbertkrebbers said

I let you merge it when you have time to fix the reverse deps. I might be able to help, but not today.

merged

mentioned in commit fe3b9967

@iris-users this renames an existing lemma

- Rename `insert_delete` → `insert_delete_insert`; add new `insert_delete` that
  is consistent with `delete_insert`.

sed script

sed -i -E 's/\binsert_delete\b/insert_delete_insert/g' $(find theories -name "*.v")