Gerwin Klein
a424d55e3e
licenses: convert license tags to SPDX
2020-03-13 14:38:24 +08:00
Victor Phan
f2d1f5ada7
refine/crefine: convert crunch with multiple constants into crunches
2020-02-03 16:29:19 +11:00
Victor Phan
285c47f622
cleanup for crunch_ignore in refine and crefine for all arches
...
Several constants are are added to the top level crunch_ignore statement in
Bits_R.thy, then removed from individual crunch statements across Refine and
CRefine.
2020-02-03 16:29:18 +11:00
Gerwin Klein
72032d8495
riscv refine: cleanup in Finalise_R
2019-11-12 18:28:39 +11:00
Gerwin Klein
4bd67d3c4e
riscv refine: clean up theory imports + fix fallout
2019-11-12 18:28:39 +11:00
Gerwin Klein
3f5aaa6c48
riscv refine: Finalise_R sorry-free
2019-11-12 18:28:39 +11:00
Gerwin Klein
cd70459771
riscv refine: reduce sorries in Finalise_R
2019-11-12 18:28:39 +11:00
Gerwin Klein
5ee57f72fc
riscv refine: sorrying Finalise_R (3 sorries)
2019-11-12 18:28:39 +11:00