squash Trace_Monad_Equations: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Mar 22, 2024 · ee3bc64 · ee3bc64
1 parent 4089a16
commit ee3bc64
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy
@@ -413,11 +413,11 @@ lemma monad_eq_split_tail:
 
 lemma double_gets_drop_regets:
   "(do x \<leftarrow> gets f;
-       xa \<leftarrow> gets f;
-       m xa x
+       y \<leftarrow> gets f;
+       m y x
     od) =
-   (do xa \<leftarrow> gets f;
-       m xa xa
+   (do x \<leftarrow> gets f;
+       m x x
     od)"
   by (simp add: simpler_gets_def bind_def)