Skip to content
Proof PR

arch-split Refine up to InvariantUpdates_H #3168

Sign in to view logs

arch-split Refine up to InvariantUpdates_H

arch-split Refine up to InvariantUpdates_H #3168

GitHub Actions / File annotations for theory linter succeeded Feb 16, 2025 in 0s

File annotations for theory linter

Annotations

Check failure on line 19 in proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

See this annotation in the file changed.

@github-actions 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 19 in proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy

See this annotation in the file changed.

@github-actions 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.
View more details on GitHub Actions