Gerwin Klein
Gerwin Klein
Pulls in license change and content update of the Simpl session from the AFP. The license changes from LGPL to BSD-3-Clause. Flow-on breakage seems to be low, the main things...
It looks like this would be relatively easy to add to #649, and could absolve one from trying to figure out the correct `if` splitting rule for the situation.
See the discussion in #649, in particular, Corey [pointing out][0] that `ccorres` probably has the same issue. For `ccorres` it would make a lot of sense to additionally split on...
In `CALL` and `PROC `, the pretty printer inserts the internal `_'proc` in the output. It should not.
Produce a `_def` theorem for the value type that provides direct symbolic access to the right-hand side of the `value_type` definition. This avoids having to unfold those terms in subsequent...
The Haskell translator might be able to work on separate files in parallel. We should investigate if that is the case, because on machines with a bunch of cores this...
On RISCV64, `Platform.thy` has nicely consistent, but outdated style. We should apply the current style guide to this file (and probably the other files in `machine/`) on all platforms to...
The name `kernel_base` is from ancient times before terminology had settled. We should converge name between ASpec, Haskell and C to avoid confusion and wasting time tracing which constants correspond....
We use a lemma set `bit_simps` in X64, RISCV64, and AARCH64. In one of the last Isabelle/Word_Lib updates, Florian also introduced a lemma set `bit_simps` mostly for rules about the...
`abs_typ_at_lifts` currently lifts over generic predicates. We likely don't want to include arch specific predicates in the generic lemma set, but we might want to create a named theorem set...