ainvs: remove hoare_seq_ext[wp] declaration

This is no longer necessary now that the nondet monad setup already makes it a wp rule. Signed-off-by: Corey Lewis <[email protected]>
seL4 · Apr 22, 2024 · 3ce8811 · 3ce8811
1 parent fe1bbae
commit 3ce8811
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy
@@ -1146,8 +1146,6 @@ lemma hy_inv: "(\<And>s f. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace
   apply (wp | simp)+
   done
 
-declare hoare_seq_ext[wp]
-
 lemma ct_active_simple [elim!]:
   "ct_active s \<Longrightarrow> st_tcb_at simple (cur_thread s) s"
   by (fastforce simp: ct_in_state_def elim!: pred_tcb_weakenE)