lib: consistent Trace filename prefix

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Jul 19, 2023 · dea1bb8 · dea1bb8
1 parent a8e7256
commit dea1bb8
Show file tree

Hide file tree

Showing 9 changed files with 13 additions and 13 deletions.
diff --git 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
@@ -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
@@ -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/
diff --git 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 → lib/Monads/trace/Trace_Lemmas.thy b/lib/Monads/trace/TraceMonadLemmas.thy → 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 → lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/TraceMonad.thy → 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 → lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/TraceMonadVCG.thy → 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
@@ -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
@@ -6,7 +6,7 @@
 theory Triv_Refinement
 
 imports
-  "Monads.TraceMonadVCG"
+  "Monads.Trace_VCG"
   "Monads.Strengthen"
 
 begin