[squash] aarch64 crefine: fix up cleanInvalidateCacheRange_RAM_ccorres #2890
File annotations for theory linter
Annotations
Check failure on line 1755 in proof/crefine/AARCH64/Fastpath_C.thy
github-actions / File annotations for theory linter
Unfinished proof
This command indicates an unfinished or aborted proof.
Check failure on line 2571 in proof/crefine/AARCH64/Fastpath_C.thy
github-actions / File annotations for theory linter
Unfinished proof
This command indicates an unfinished or aborted proof.
Check failure on line 549 in proof/crefine/AARCH64/Fastpath_Equiv.thy
github-actions / File annotations for theory linter
Unfinished proof
This command indicates an unfinished or aborted proof.
Check failure on line 1423 in proof/crefine/AARCH64/Fastpath_Equiv.thy
github-actions / File annotations for theory linter
Unfinished proof
This command indicates an unfinished or aborted proof.
Check failure on line 17 in proof/crefine/AARCH64/Init_C.thy
github-actions / File annotations for theory linter
Axioms
Locales or definitions should usually be preferred to axioms, because axioms may make the logic inconsistent. Merely introducing a new constant (without new laws) is fine, though.