diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy
index 49ce6f403c..e7966c63b8 100644
--- a/lib/Crunch_Instances_Trace.thy
+++ b/lib/Crunch_Instances_Trace.thy
@@ -7,7 +7,7 @@
 theory Crunch_Instances_Trace
 imports
   Crunch
-  Monads.TraceMonadVCG
+  Monads.Trace_VCG
 begin
 
 lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE
diff --git a/lib/Monads/Monad_Lib.thy b/lib/Monads/Monad_Lib.thy
index 59add57c08..9147968b1c 100644
--- a/lib/Monads/Monad_Lib.thy
+++ b/lib/Monads/Monad_Lib.thy
@@ -5,7 +5,7 @@
  *)
 
 (* This theory collects the minimum constant definitions and lemmas for the monad definition
-   theories (Nondet_Monad, TraceMonad etc). Only things that are necessary for these and needed
+   theories (Nondet_Monad, Trace_Monad etc). Only things that are necessary for these and needed
    by more than one of them should go in here. *)
 
 theory Monad_Lib
diff --git a/lib/Monads/README.md b/lib/Monads/README.md
index 4345c6b2ef..28d00f00e1 100644
--- a/lib/Monads/README.md
+++ b/lib/Monads/README.md
@@ -35,5 +35,5 @@ in weakest-precondition style.
 [l4v]: https://github.com/seL4/l4v/
 [nondet]: ./nondet/Nondet_Monad.thy
 [option]: ./reader_option/Reader_Option_Monad.thy
-[trace]: ./trace/TraceMonad.thy
+[trace]: ./trace/Trace_Monad.thy
 [AutoCorres]: ../../tools/autocorres/
\ No newline at end of file
diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT
index c13eb42d2f..284039d3ba 100644
--- a/lib/Monads/ROOT
+++ b/lib/Monads/ROOT
@@ -22,17 +22,17 @@ session Monads (lib) = HOL +
 
   theories
     Nondet_WhileLoopRules
-    TraceMonad
+    Trace_Monad
     Reader_Option_ND
     Reader_Option_VCG
     Strengthen_Demo
-    TraceMonadLemmas
+    Trace_Lemmas
     Datatype_Schematic
     Nondet_WhileLoopRulesCompleteness
     Strengthen
     Nondet_Strengthen_Setup
     Reader_Option_Monad
-    TraceMonadVCG
+    Trace_VCG
     Nondet_In_Monad
     Nondet_VCG
     Nondet_Sat
diff --git a/lib/Monads/trace/TraceMonadLemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy
similarity index 99%
rename from lib/Monads/trace/TraceMonadLemmas.thy
rename to lib/Monads/trace/Trace_Lemmas.thy
index 45e4aedbeb..6b5533d811 100644
--- a/lib/Monads/trace/TraceMonadLemmas.thy
+++ b/lib/Monads/trace/Trace_Lemmas.thy
@@ -3,8 +3,8 @@
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
-theory TraceMonadLemmas
-imports TraceMonadVCG
+theory Trace_Lemmas
+imports Trace_VCG
 begin
 
 lemma mapM_Cons:
diff --git a/lib/Monads/trace/TraceMonad.thy b/lib/Monads/trace/Trace_Monad.thy
similarity index 99%
rename from lib/Monads/trace/TraceMonad.thy
rename to lib/Monads/trace/Trace_Monad.thy
index 891d17ebec..506f8954ca 100644
--- a/lib/Monads/trace/TraceMonad.thy
+++ b/lib/Monads/trace/Trace_Monad.thy
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
-theory TraceMonad
+theory Trace_Monad
 imports
   Monad_Lib
   Strengthen
diff --git a/lib/Monads/trace/TraceMonadVCG.thy b/lib/Monads/trace/Trace_VCG.thy
similarity index 99%
rename from lib/Monads/trace/TraceMonadVCG.thy
rename to lib/Monads/trace/Trace_VCG.thy
index fb75b3027e..9bdc420918 100644
--- a/lib/Monads/trace/TraceMonadVCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -3,9 +3,9 @@
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
-theory TraceMonadVCG
+theory Trace_VCG
 imports
-  TraceMonad
+  Trace_Monad
   Fun_Pred_Syntax
   WPSimp
 begin
diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy
index 336f673b89..774d3360f6 100644
--- a/lib/concurrency/Prefix_Refinement.thy
+++ b/lib/concurrency/Prefix_Refinement.thy
@@ -7,7 +7,7 @@ theory Prefix_Refinement
 
 imports
   Triv_Refinement
-  "Monads.TraceMonadLemmas"
+  "Monads.Trace_Lemmas"
 
 begin
 
diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy
index 85ef2fd96f..caefd59834 100644
--- a/lib/concurrency/Triv_Refinement.thy
+++ b/lib/concurrency/Triv_Refinement.thy
@@ -6,7 +6,7 @@
 theory Triv_Refinement
 
 imports
-  "Monads.TraceMonadVCG"
+  "Monads.Trace_VCG"
   "Monads.Strengthen"
 
 begin