aarch64 crefine: update to match other arches

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Mar 27, 2024 · 9d6443a · 9d6443a
1 parent e98ecec
commit 9d6443a
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: