fix naming conflict causing errors in InfoFlowC

Signed-off-by: Michael McInerney <[email protected]>
seL4 · May 8, 2024 · b914ce2 · b914ce2
1 parent 1c54809
commit b914ce2
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/proof/infoflow/refine/ADT_IF_Refine.thy b/proof/infoflow/refine/ADT_IF_Refine.thy
@@ -509,7 +509,7 @@ lemma scheduler'_if_ex_abs[wp]:
    apply wp
   apply (clarsimp simp: ex_abs_def)
   apply (rule exI, rule conjI, assumption)
-  apply (frule state_relation_schact)
+  apply (frule state_relation_sched_act_relation)
   apply (auto simp: domain_list_rel_eq domain_time_rel_eq)
   done
 

diff --git a/proof/refine/ARM/StateRelation.thy b/proof/refine/ARM/StateRelation.thy
@@ -654,14 +654,14 @@ lemma state_relation_pspace_relation[elim!]:
   "(s,s') \<in> state_relation \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')"
   by (simp add: state_relation_def)
 
-lemma state_relation_schact[elim!]:
-  "(s,s') \<in> state_relation \<Longrightarrow> sched_act_relation (scheduler_action s) (ksSchedulerAction s')"
-  by (simp add: state_relation_def)
-
 lemma state_relation_ekheap_relation[elim!]:
   "(s,s') \<in> state_relation \<Longrightarrow> ekheap_relation (ekheap s) (ksPSpace s')"
   by (simp add: state_relation_def)
 
+lemma state_relation_sched_act_relation[elim!]:
+  "(s,s') \<in> state_relation \<Longrightarrow> sched_act_relation (scheduler_action s) (ksSchedulerAction s')"
+  by (clarsimp simp: state_relation_def)
+
 lemma state_relation_ready_queues_relation[elim!]:
   "(s, s') \<in> state_relation \<Longrightarrow> ready_queues_relation s s'"
   by (simp add: state_relation_def)