lib: adjust corres_symb_exec_r_conj_ex_abs_forwards

This was required after a recent update to the schematics of corres_symb_exec_r_conj_ex_abs Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jul 15, 2024 · e429ff6 · e429ff6
1 parent a30419f
commit e429ff6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy
@@ -308,7 +308,7 @@ proof -
 qed
 
 lemmas corres_symb_exec_r_conj_ex_abs_forwards =
-  corres_symb_exec_r_conj_ex_abs[where P'=P' and Q'=P' for P', simplified]
+  corres_symb_exec_r_conj_ex_abs[where P=P and Q=P for P, where P'=P' and Q'=P' for P', simplified]
 
 lemma gets_the_corres_ex_abs':
  "\<lbrakk>no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\<rbrakk> \<Longrightarrow>