fix indent squash into mapM rules

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Dec 19, 2024 · 96a3752 · 96a3752
1 parent aa8cfff
commit 96a3752
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/Monad_Lists.thy b/lib/Monad_Lists.thy
@@ -516,7 +516,7 @@ lemma mapM_gets_the_wp:
   "\<lbrace>\<lambda>s. \<forall>vs. map (\<lambda>t. f t s) ts = map Some vs \<longrightarrow> P vs s\<rbrace>
    mapM (gets_the \<circ> f) ts
    \<lbrace>P\<rbrace>"
-unfolding comp_def
+  unfolding comp_def
 proof (induct ts arbitrary: P)
   case Nil thus ?case by (wpsimp simp: mapM_Nil)
 next