Gerwin Klein

I 'm fine the first two (pretty left, standard right), and can live with the naive left version as well, so those are all good. I guess variant 1 and...

Agreed, I would probably also not put the `in` line in the previous line as the comment says. The only exception would be if everything fits on one line anyway....

This is not trying to be comprehensive, but just an improvement to the "sorry, no clue" that was there before.

> When looking at this PR, I kept having a sneaking suspicion I had written about something related already and asked people for feedback, although I couldn't find the direct...

> Something to consider w.r.t. a "proving False" vs a "unprovable subterms" section, is that I rarely get to see a proper `False`. Especially in larger goals, the "why do...

Now updated with Raf's gist as a basis and extracted from the CRefine notes as a separate file. I also added all our recent new files to the README, which...

> Thanks for resolving this, I think the outcome looks good now, only had trivial nitpicks. Time will tell whether anyone actually goes and looks at the debugging guide, but...

It looks like this does need a verification update, because we have some of these values replicated in the spec. I'll have a look at that.

The `"` in the output is part of the Isabelle syntax, i.e. what we want to produce are strings like ```isabelle definition x :: "some_type \ some_other_type" where ``` Using...

> It should be safe to make this change. > [..] > When the RISC-V port was up-streamed, it didn't restore the register with the other registers, but also didn't...