aarch64 orphanage: handleHypervisorFault_no_orphans #2881
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.
Check failure on line 2775 in proof/crefine/AARCH64/IpcCancel_C.thy
github-actions / File annotations for theory linter
Unfinished proof
This command indicates an unfinished or aborted proof.
Check failure on line 2950 in proof/crefine/AARCH64/IpcCancel_C.thy
github-actions / File annotations for theory linter
Unfinished proof
This command indicates an unfinished or aborted proof.