From 42ef688160f2050ad061feac7f41f7effd822b00 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Wed, 27 Mar 2024 14:40:54 +1030
Subject: [PATCH] remove extra space and rename variable in
 corres_cross_add_guard

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/Corres_UL.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
index 031f758bf0..733f09316e 100644
--- 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)