Gerwin Klein

Ideally we'd do this by cherry-picking the relevant commits similar to #468. This only works if proof adjustments are minimal. The list of files with relevant differences currently is: -...

I don't think there is one in the `master` branch yet, but there is a pull request (#147) that has a commit c02ecd9e3ca57333226729e317b2f542f458f4ae which introduces the rule for `corres_underlying`. You...

Those two monads generally do not correspond, because they behave differently -- one can return errors and the other not. Usually there is something like a `liftE` on the error...

We don't have an exception version yet, sorry. You'll have to prove one yourself, but we'd be happy to take a pull request to add it to the library.

Thanks @noneGMJ, it looks like with a bit more fine-tuning we could include that in the library.

And as soon as I was typing this out, it occurred to me that we can easily do this with an input abbreviation. E.g. ```isabelle abbreviation lifted where "lifted P...

Potential syntax form: `P`

Playing a bit more with this, it looks like the code generator gadget is in fact messing up something and is no longer needed in Isabelle2021-1. If I try `value`...

After doing all the bits, the checks in in #470 revealed that there is some usage left -- not of the proof method (we should still remove that one), but...

@mbrcknl do you have time to look into this, or should I have a go later this week? We're currently not deploying any more to the verification manifest, so we...