From e429ff680a10890ebee3127db03b728374d069e6 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 15 Jul 2024 13:40:28 +0930 Subject: [PATCH] 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 --- lib/ExtraCorres.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index 849c783000..c8f0ed7774 100644 --- 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': "\no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\ \