squash into no_trace rule set: remove FIXME

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Jan 31, 2024 · 4cdfa4e · 4cdfa4e
1 parent 086f94a
commit 4cdfa4e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/lib/Monads/trace/Trace_No_Trace.thy b/lib/Monads/trace/Trace_No_Trace.thy
@@ -348,8 +348,8 @@ lemma no_trace_andM[no_trace_cond]:
   unfolding andM_def
   by (wpsimp wp: no_trace_terminal no_trace_cond)
 
-\<comment> \<open>FIXME: This is true but is it useful to even state?
-          The parallel composition of traceless functions doesn't make much sense\<close>
+\<comment> \<open>While the parallel composition of traceless functions doesn't make much sense, this
+   still might be useful to handle trivial goals as part of a proof by contradiction.\<close>
 lemma no_trace_parallel[no_trace_cond]:
   "\<lbrakk> no_trace f; no_trace g \<rbrakk> \<Longrightarrow> no_trace (parallel f g)"
   by (fastforce simp: parallel_def2 no_trace_def)