diff --git a/lib/Monads/trace/Trace_Prefix_Closed.thy b/lib/Monads/trace/Trace_Prefix_Closed.thy
index 04e0a90f0f..63597206c3 100644
--- a/lib/Monads/trace/Trace_Prefix_Closed.thy
+++ b/lib/Monads/trace/Trace_Prefix_Closed.thy
@@ -14,6 +14,9 @@ begin
 
 subsection "Prefix Closed"
 
+text \<open>
+  A monad is prefix_closed if for all traces that it returns, it also returns all incomplete traces
+  leading up to it.\<close>
 definition prefix_closed :: "('s, 'a) tmonad \<Rightarrow> bool" where
   "prefix_closed f = (\<forall>s. \<forall>x xs. (x # xs) \<in> fst ` f s \<longrightarrow> (xs, Incomplete) \<in> f s)"