remove extra space and rename variable in corres_cross_add_guard

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Mar 27, 2024 · a53b39b · a53b39b
1 parent d593972
commit a53b39b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
@@ -1177,8 +1177,8 @@ lemma corres_move_asm:
 lemmas corres_cross_over_guard = corres_move_asm[rotated]
 
 lemma corres_cross_add_guard:
-  "\<lbrakk> \<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q s';
-     corres_underlying sr nf nf' r P  (P' and Q) f g\<rbrakk>
+  "\<lbrakk> \<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q' s';
+     corres_underlying sr nf nf' r P (P' and Q') f g\<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
   by (fastforce simp: corres_underlying_def)