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 <[email protected]>
seL4 · Apr 2, 2024 · 1e9ce18 · 1e9ce18
1 parent e98ecec
commit 1e9ce18
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 "\<And>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: