[squash] aarch64 crefine: fix up cleanInvalidateCacheRange_RAM_ccorres #2890
Annotations
5 errors
Unfinished proof:
proof/crefine/AARCH64/Fastpath_C.thy#L1755
This command indicates an unfinished or aborted proof.
|
Unfinished proof:
proof/crefine/AARCH64/Fastpath_C.thy#L2571
This command indicates an unfinished or aborted proof.
|
Unfinished proof:
proof/crefine/AARCH64/Fastpath_Equiv.thy#L549
This command indicates an unfinished or aborted proof.
|
Unfinished proof:
proof/crefine/AARCH64/Fastpath_Equiv.thy#L1423
This command indicates an unfinished or aborted proof.
|
Axioms:
proof/crefine/AARCH64/Init_C.thy#L17
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.
|