Gerwin Klein

- [x] commit msg of the first commit should mention `Simpl` not just `c-parser`.

> Looks good! > > It's very minor, but I'm not sure that we gain anything from all of the Simpl updates being separate commits. We can probably squash all...

> These are quite large diffs to SIMPL, it's interesting that there's not more fallout for us. Wonder if we'll get any improvements in the term printing speed at some...

In particular also between `rt` and `master`

> It would be good to propagate the last two back to the Hoare versions, to keep things consistent and allow us to update the rest of the proofs now....

We should really track down the pairs when we have some time. `wpfix` should be able to deal with them (or `datatype_schem` which is called by `wpfix`), and if it...

> * changing `no_pre` to `classic_wp_pre` in any broken proofs. This is a different bundle that (I'm assuming) returns the attributes to how they were before `wp_pre` was implemented. In...

That strange `declare hoare_seq_ext[wp]` is from a commit by Matthias (still in `hg` back then, on branch `virtual-memory`) from 2012. The commit is fairly large and adds a number of...

> Another issue that I've just discovered is that `wp (once)` doesn't invoke `wp_pre` and there are several instances where it was instead using `hoare_vcg_precond_imp` as a `wp_comb` rule to...

So `wp_pre0` and `wpfix` should only be applicable once to a specific goal, i.e. once they have applied they should not be able to apply again. So that would be...