From a82ad0b99e971f0f315089556422b608a4247a74 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Wed, 27 Mar 2024 12:25:14 +1100 Subject: [PATCH] aarch64 crefine: update to match other arches This corresponds to a change made in 146eaa1, following adjustments to some no_fail attributes. Signed-off-by: Corey Lewis --- proof/crefine/AARCH64/VSpace_C.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy index cbd5fc12ba..745f91e322 100644 --- a/proof/crefine/AARCH64/VSpace_C.thy +++ b/proof/crefine/AARCH64/VSpace_C.thy @@ -335,7 +335,7 @@ lemma corres_symb_exec_unknown_r: assumes "\rv. corres_underlying sr nf nf' r P P' a (c rv)" shows "corres_underlying sr nf nf' r P P' a (unknown >>= c)" apply (simp add: unknown_def) - apply (rule corres_symb_exec_r[OF assms]; wp select_inv no_fail_select) + apply (rule corres_symb_exec_r[OF assms]; wp select_inv) done lemma isPageTablePTE_def2: