From e59522cfd79467056a36bf1bb93f415103b41f27 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Wed, 27 Mar 2024 15:28:18 +1030
Subject: [PATCH] reindent corres_cross_add_guard and friend squash

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

diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
index 733f09316e..395a327b04 100644
--- a/lib/Corres_UL.thy
+++ b/lib/Corres_UL.thy
@@ -1177,15 +1177,15 @@ 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>
-    \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  "\<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)
 
 lemma corres_cross_add_abs_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 and Q)  P' f g\<rbrakk>
-    \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  "\<lbrakk>\<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q s;
+    corres_underlying sr nf nf' r (P and Q)  P' f g\<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
   by (fastforce simp: corres_underlying_def)
 
 lemma corres_either_alternate: