Gerwin Klein

I haven't yet used the new `_def` theorems to eliminate previous manual instance of that, because my first search&replace attempt turned out to be too aggressive. I might add another...

> I think this is a solid start (going via _val for now). Content looks good. For `aarch64` branch, we'll have to do the update as well. Maybe after pre-VSpace_C,...

I haven't checked, but the same probably applies to `typ_at_lifts` in Refine.

The problem with making such lemmas globally `[simp]` is that `P` can be an equation (or negation of an equation). That means if we rewrite to `P`, then the simplifier...

As discussed in person, I'm happy with the changes to the export script, but I think it'd be good to avoid complicating `kernel.mk` more than necessary with additional conditionals. If...

@mbrcknl should we close this PR and archive it for now? Happy for it to be re-opened when we get back to it, but currently it looks like we're not...

Will also defer until after seL4/ci-actions#332 and until we have added the camkes actions there as well.

Makes sense, I'll see if there are any specific problems in making it a separate job.

With seL4/ci-actions#332 it will be easier to manage workflows over multiple repos, so I'll defer this until we have gotten that working properly.

> The CI build is failing with include errors, but I wonder if this is related the the change here or a general probelm? It's at least not a CI...