From 2248196ed2f76fbd2f0d2dbe0c35b6323a7890f6 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 11 Sep 2024 23:27:26 +0930 Subject: [PATCH] fix error squash Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Tcb_C.thy | 1 - 1 file changed, 1 deletion(-) diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index ac68d104a2..099dba87cb 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -4684,7 +4684,6 @@ lemma decodeSetTLSBase_ccorres: apply (clarsimp simp: ct_in_state'_def sysargs_rel_n_def n_msgRegisters_def) apply (auto simp: valid_tcb_state'_def elim!: pred_tcb'_weakenE)[1] - apply (simp add: ThreadState_defs mask_eq_iff_w2p word_size) apply (frule rf_sr_ksCurThread) apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) apply (auto simp: unat_eq_0 le_max_word_ucast_id)+