reindent corres_cross_add_guard and friend squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Mar 28, 2024 · 41dd096 · 41dd096
1 parent 85fabc5
commit 41dd096
Showing 1 changed file with 6 additions and 6 deletions.
diff --git 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: