diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy
index a7440a1ca..d25bc6dbc 100644
--- a/proof/crefine/RISCV64/IpcCancel_C.thy
+++ b/proof/crefine/RISCV64/IpcCancel_C.thy
@@ -399,10 +399,10 @@ lemma ccorres_exI1:
   apply fastforce
   done
 
-lemma isBlocked_ccorres [corres]:
+lemma isStopped_ccorres [corres]:
   "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
   (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread})  []
-  (isBlocked thread) (Call isBlocked_'proc)"
+  (isStopped thread) (Call isStopped_'proc)"
   apply (cinit lift: thread_' simp: getThreadState_def)
   apply (rule ccorres_pre_threadGet)
    apply (rule ccorres_move_c_guard_tcb)
@@ -1900,8 +1900,8 @@ lemma true_eq_from_bool [simp]:
   "(scast true = from_bool P) = P"
   by (simp add: true_def from_bool_def split: bool.splits)
 
-lemma isBlocked_spec:
-  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isBlocked_'proc
+lemma isStopped_spec:
+  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isStopped_'proc
        {s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
                             {scast ThreadState_BlockedOnReply,
                              scast ThreadState_BlockedOnNotification, scast ThreadState_BlockedOnSend,
@@ -2357,7 +2357,7 @@ lemma scheduleTCB_ccorres':
            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                  cscheduler_action_relation_def)
           apply wp+
-     apply (simp add: isRunnable_def isBlocked_def)
+     apply (simp add: isRunnable_def isStopped_def)
     apply wp
    apply (simp add: guard_is_UNIV_def)
   apply clarsimp
@@ -2413,7 +2413,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
            apply (clarsimp simp: rf_sr_def cstate_relation_def cscheduler_action_relation_def
                            split: scheduler_action.split_asm)
           apply wp+
-     apply (simp add: isRunnable_def isBlocked_def)
+     apply (simp add: isRunnable_def isStopped_def)
     apply wp
    apply (simp add: guard_is_UNIV_def)
   apply (clarsimp simp: st_tcb_at'_def obj_at'_def)
@@ -2504,7 +2504,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
            apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                  cscheduler_action_relation_def)
           apply wp+
-     apply (simp add: isRunnable_def isBlocked_def)
+     apply (simp add: isRunnable_def isStopped_def)
     apply wp
    apply (simp add: guard_is_UNIV_def)
   apply clarsimp
diff --git a/proof/crefine/RISCV64/IsolatedThreadAction.thy b/proof/crefine/RISCV64/IsolatedThreadAction.thy
index 5c8fe33d2..95ec02945 100644
--- a/proof/crefine/RISCV64/IsolatedThreadAction.thy
+++ b/proof/crefine/RISCV64/IsolatedThreadAction.thy
@@ -807,7 +807,7 @@ lemma rescheduleRequired_simple_rewrite:
 
 lemma empty_fail_isRunnable:
   "empty_fail (isRunnable t)"
-  by (simp add: isRunnable_def isBlocked_def)
+  by (simp add: isRunnable_def isStopped_def)
 
 lemma setupCallerCap_rewrite:
   "monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))
@@ -909,7 +909,7 @@ lemma oblivious_switchToThread_schact:
                    getCurThread_def setCurThread_def threadGet_def liftM_def
                    threadSet_def tcbSchedEnqueue_def unless_when asUser_def
                    getQueue_def setQueue_def storeWordUser_def setRegister_def
-                   pointerInUserData_def isRunnable_def isBlocked_def
+                   pointerInUserData_def isRunnable_def isStopped_def
                    getThreadState_def tcbSchedDequeue_def bitmap_fun_defs)
   by (safe intro!: oblivious_bind
               | simp_all add: oblivious_setVMRoot_schact)+
diff --git a/proof/crefine/RISCV64/Syscall_C.thy b/proof/crefine/RISCV64/Syscall_C.thy
index 43a34ec80..7126c8051 100644
--- a/proof/crefine/RISCV64/Syscall_C.thy
+++ b/proof/crefine/RISCV64/Syscall_C.thy
@@ -1413,7 +1413,7 @@ lemma handleRecv_ccorres:
                 auto simp: pred_tcb_at'_def obj_at'_def objBits_simps projectKOs ct_in_state'_def)[1]
          apply wp
      apply clarsimp
-     apply (vcg exspec=isBlocked_modifies exspec=lookupCap_modifies)
+     apply (vcg exspec=isStopped_modifies exspec=lookupCap_modifies)
 
     apply wp
    apply clarsimp
diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy
index 68b038bd2..79de809b3 100644
--- a/proof/crefine/RISCV64/Tcb_C.thy
+++ b/proof/crefine/RISCV64/Tcb_C.thy
@@ -1084,7 +1084,7 @@ lemma restart_ccorres:
         (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) []
      (restart thread) (Call restart_'proc)"
   apply (cinit lift: target_')
-   apply (ctac(no_vcg) add: isBlocked_ccorres)
+   apply (ctac(no_vcg) add: isStopped_ccorres)
     apply (simp only: when_def)
     apply (rule ccorres_cond2[where R=\<top>])
       apply (simp add: to_bool_def Collect_const_mem)