Did you run diffpdf on this, and did you check whether it copy-pastes as expected?

I did check selected instances that they copy-pasted as the ASCII caret character (verified with "od -x" on the resulting text file).
I've just run diffpdf, and it looks "good" (i.e. one caret character replaced by a slightly-different caret character), as expected.

Great, thanks! We may hold off on merging until the motions are in; this is a somewhat big change and I'd prefer not to risk having to rebase a lot.

I've redone the patch because a space went missing in two places for bit_xor (clause 20). \caret{} as opposed to \caret seems to have fixed that.

Can we redefine \^ as \caret, or are we still using the original for something?

@zygoloid Messing with catcodes? Hmmm. I'm sure it can be done, but should it?

\catcode`^=\active
\newcommand{^}{\char`\^}

(And of course you'd need to make sure you don't change the catcode in math mode... I would be very hesitant to pursue this direction.)

This may have a race with the indexing-atomics pull request, which adds additional use of carets in the index, clearly using the older formulation for now.

@AlisdairM: without fishing for a pun here, a lot of things will be racing on atomics. Please be patient and rebase a lot. I'm about to push yet another unrelated change.

@jensmaurer: I'd say rebase and resolve this, and we'll merge this now. All the NB comments have been resolved, and we can fix up the motion applications if necessary.

@tkoeppe the atomics indexing branch should be fairly idempotent, as few changes tend to peek in there. This is the one race I know about, and happy to fix up atomics if this lands first. Note that I will not be available for the following three weeks, starting in around 24 hours, so it would be nice to land before then if possible - if not, we will catch up for next time, no problem.

@jensmaurer: Ping, any chance you can get this PR resolved before Alisdair leaves?

Don't worry - I can see the PRs that just landed, that Thomas was referring to. I'll fix the atomics branch up again tonight, and should leave it in a state that is easy for someone else to pick up and land while I am gone - don't want to further distract /this/ review!

I didn't see there was a conflict meanwhile. Fixed.