diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
index 5357a6a9d..f3b7e3d28 100644
--- a/lib/Corres_UL.thy
+++ b/lib/Corres_UL.thy
@@ -7,8 +7,8 @@
 theory Corres_UL
 imports
   Crunch_Instances_NonDet
-  WPEx
-  WPFix
+  Monads.WPEx
+  Monads.WPFix
   HaskellLemmaBucket
 begin
 
diff --git a/lib/Crunch.thy b/lib/Crunch.thy
index 62c0996f6..c47955e1d 100644
--- a/lib/Crunch.thy
+++ b/lib/Crunch.thy
@@ -6,7 +6,7 @@
 
 theory Crunch
 imports
-  WPSimp
+  Monads.WPSimp
   Lib
   ML_Utils.ML_Utils
 keywords "crunch" "crunch_ignore" "crunches" :: thy_decl
diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy
index c21b11a63..49ce6f403 100644
--- a/lib/Crunch_Instances_Trace.thy
+++ b/lib/Crunch_Instances_Trace.thy
@@ -7,7 +7,7 @@
 theory Crunch_Instances_Trace
 imports
   Crunch
-  TraceMonadVCG
+  Monads.TraceMonadVCG
 begin
 
 lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE
diff --git a/lib/EVTutorial/EquivValidTutorial.thy b/lib/EVTutorial/EquivValidTutorial.thy
index 801558eab..55723d005 100644
--- a/lib/EVTutorial/EquivValidTutorial.thy
+++ b/lib/EVTutorial/EquivValidTutorial.thy
@@ -55,7 +55,7 @@ In this sense, EquivValid statements could be thought of as \<^emph>\<open>relat
 
 text \<open> This tutorial will introduce some syntactic sugar to emphasise the similarity
 between Hoare triples and EquivValid statements.
-(Here, \<open>\<top>\<top>\<close> is an alias provided by Lib.NonDetMonad for the trivial binary predicate,
+(Here, \<open>\<top>\<top>\<close> is an alias provided by Monads.NonDetMonad for the trivial binary predicate,
 which always returns \<open>True\<close>; similarly, there is also \<open>\<bottom>\<bottom>\<close> for \<open>False\<close>.) \<close>
 
 abbreviation
@@ -140,7 +140,7 @@ where
 text \<open> We could just as well define equivalences similarly for
 \<open>inbox\<close>, \<open>outbox\<close>, or \<open>job\<close> -- we omit these here. \<close>
 
-text \<open> Furthermore, you can use the \<open>and\<close> alias provided by @{theory Lib.Fun_Pred_Syntax}
+text \<open> Furthermore, you can use the \<open>and\<close> alias provided by @{theory Monads.Fun_Pred_Syntax}
 to write the conjunction of two binary predicates.
 (Similarly, there is also an \<open>or\<close> alias for disjunction.)\<close>
 
diff --git a/lib/EmptyFailLib.thy b/lib/EmptyFailLib.thy
index b8b93f7e5..68309c7fb 100644
--- a/lib/EmptyFailLib.thy
+++ b/lib/EmptyFailLib.thy
@@ -6,7 +6,7 @@
 
 theory EmptyFailLib
 imports
-  NonDetMonad
+  Monads.NonDetMonad
   HaskellLib_H
 begin
 
diff --git a/lib/Extract_Conjunct.thy b/lib/Extract_Conjunct.thy
index 03feba42e..b9986c482 100644
--- a/lib/Extract_Conjunct.thy
+++ b/lib/Extract_Conjunct.thy
@@ -7,7 +7,7 @@
 theory Extract_Conjunct
 imports
   "Main"
-  "Eisbach_Methods"
+  Eisbach_Tools.Eisbach_Methods
 begin
 
 section \<open>Extracting conjuncts in the conclusion\<close>
diff --git a/lib/GenericLib.thy b/lib/GenericLib.thy
index 18eb72ba1..f4004d7a5 100644
--- a/lib/GenericLib.thy
+++ b/lib/GenericLib.thy
@@ -7,7 +7,7 @@
 theory GenericLib
 imports
   Crunch_Instances_NonDet
-  WPEx
+  Monads.WPEx
   HaskellLemmaBucket
 begin
 
diff --git a/lib/Guess_ExI.thy b/lib/Guess_ExI.thy
index 7fd4ce52a..875fb814f 100644
--- a/lib/Guess_ExI.thy
+++ b/lib/Guess_ExI.thy
@@ -6,8 +6,8 @@
 
 theory Guess_ExI
 imports
-  Eisbach_Methods
-  Apply_Debug
+  Eisbach_Tools.Eisbach_Methods
+  Eisbach_Tools.Apply_Debug
 begin
 
 (*
diff --git a/lib/LexordList.thy b/lib/LexordList.thy
index f5beecc10..3dee0a806 100644
--- a/lib/LexordList.thy
+++ b/lib/LexordList.thy
@@ -6,7 +6,7 @@
 
 theory LexordList imports
   Main
-  Eisbach_Methods (* for tests *)
+  Eisbach_Tools.Eisbach_Methods (* for tests *)
 begin
 
 text \<open>
diff --git a/lib/Lib.thy b/lib/Lib.thy
index 17887a291..233de7e1c 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -18,8 +18,8 @@ imports
   Extract_Conjunct
   ML_Goal
   Eval_Bool
-  Fun_Pred_Syntax
-  Monad_Lib
+  Monads.Fun_Pred_Syntax
+  Monads.Monad_Lib
   NICTATools
   "Word_Lib.WordSetup"
 begin
diff --git a/lib/Monad_Equations.thy b/lib/Monad_Equations.thy
index c4f0cc606..2362003b6 100644
--- a/lib/Monad_Equations.thy
+++ b/lib/Monad_Equations.thy
@@ -9,7 +9,7 @@
    Should not be Hoare triples (those go into a different theory). *)
 
 theory Monad_Equations
-  imports MonadEq_Lemmas
+  imports Monads.MonadEq_Lemmas
 begin
 
 lemmas assertE_assert = assertE_liftE
diff --git a/lib/NICTATools.thy b/lib/NICTATools.thy
index 6d42c7c09..5fc6acaf5 100644
--- a/lib/NICTATools.thy
+++ b/lib/NICTATools.thy
@@ -7,16 +7,16 @@
 (* Miscellaneous Isabelle tools. *)
 theory NICTATools
 imports
-  Apply_Trace_Cmd
-  Apply_Debug
+  Eisbach_Tools.Apply_Trace_Cmd
+  Eisbach_Tools.Apply_Debug
   Find_Names
   (* Solves_Tac *)
-  Rule_By_Method
-  Eisbach_Methods
+  Eisbach_Tools.Rule_By_Method
+  Eisbach_Tools.Eisbach_Methods
   Time_Methods_Cmd
   Try_Attribute
   Repeat_Attribute
-  Trace_Schematic_Insts
+  Eisbach_Tools.Trace_Schematic_Insts
   Insulin
   ShowTypes
   Locale_Abbrev
diff --git a/lib/ROOT b/lib/ROOT
index d097b06f2..220011d46 100644
--- a/lib/ROOT
+++ b/lib/ROOT
@@ -19,11 +19,9 @@ session Lib (lib) = Word_Lib +
     List_Lib
     SubMonadLib
     Simulation
-    MonadEq
     SimpStrategy
     Extract_Conjunct
     GenericLib
-    ProvePart
     Corres_Adjust_Preconds
     Requalify
     Value_Abbreviation
@@ -41,7 +39,6 @@ session Lib (lib) = Word_Lib +
     Try_Methods
     ListLibLemmas
     Time_Methods_Cmd
-    Apply_Debug
     MonadicRewrite
     HaskellLemmaBucket
     FP_Eval
@@ -122,7 +119,6 @@ session LibTest (lib) in test = Refine +
     RangeMap_Test
     FP_Eval_Tests
     Trace_Schematic_Insts_Test
-    Local_Method_Tests
     Qualify_Test
     Locale_Abbrev_Test
     Value_Type_Test
diff --git a/lib/Try_Methods.thy b/lib/Try_Methods.thy
index 238e7a873..a4aa2ce97 100644
--- a/lib/Try_Methods.thy
+++ b/lib/Try_Methods.thy
@@ -6,7 +6,7 @@
 
 theory Try_Methods
 
-imports Eisbach_Methods
+imports Eisbach_Tools.Eisbach_Methods
 
 keywords "trym" :: diag
   and "add_try_method" :: thy_decl
diff --git a/lib/clib/BitFieldProofsLib.thy b/lib/clib/BitFieldProofsLib.thy
index 25556d347..e0dd8145f 100644
--- a/lib/clib/BitFieldProofsLib.thy
+++ b/lib/clib/BitFieldProofsLib.thy
@@ -6,7 +6,7 @@
 
 theory BitFieldProofsLib
 imports
-  "Lib.Eisbach_Methods"
+  "Eisbach_Tools.Eisbach_Methods"
   TypHeapLib
 begin
 
diff --git a/lib/clib/Simpl_Rewrite.thy b/lib/clib/Simpl_Rewrite.thy
index 62d229f3a..26b5e4b68 100644
--- a/lib/clib/Simpl_Rewrite.thy
+++ b/lib/clib/Simpl_Rewrite.thy
@@ -10,8 +10,8 @@ text \<open>A simple proof method for rewriting Simpl programs under a predicate
 theory Simpl_Rewrite
 imports
   "Simpl-VCG.Vcg"
-  "Lib.Eisbach_Methods"
-  "Lib.Apply_Debug"
+  "Eisbach_Tools.Eisbach_Methods"
+  "Eisbach_Tools.Apply_Debug"
 begin
 
 text \<open>One layer of context around a Simpl program.
diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy
index cde7827b4..336f673b8 100644
--- a/lib/concurrency/Prefix_Refinement.thy
+++ b/lib/concurrency/Prefix_Refinement.thy
@@ -7,7 +7,7 @@ theory Prefix_Refinement
 
 imports
   Triv_Refinement
-  "Lib.TraceMonadLemmas"
+  "Monads.TraceMonadLemmas"
 
 begin
 
diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy
index 730276e38..85ef2fd96 100644
--- a/lib/concurrency/Triv_Refinement.thy
+++ b/lib/concurrency/Triv_Refinement.thy
@@ -6,8 +6,8 @@
 theory Triv_Refinement
 
 imports
-  "Lib.TraceMonadVCG"
-  "Lib.Strengthen"
+  "Monads.TraceMonadVCG"
+  "Monads.Strengthen"
 
 begin
 
diff --git a/lib/test/Apply_Debug_Test.thy b/lib/test/Apply_Debug_Test.thy
index b01ef6b7f..c63f53013 100644
--- a/lib/test/Apply_Debug_Test.thy
+++ b/lib/test/Apply_Debug_Test.thy
@@ -6,8 +6,8 @@
 
 theory Apply_Debug_Test
 imports
-  Lib.Apply_Debug
-  Lib.Apply_Trace_Cmd
+  Eisbach_Tools.Apply_Debug
+  Eisbach_Tools.Apply_Trace_Cmd
 begin
 
 chapter \<open>Apply_Debug\<close>
diff --git a/lib/test/Match_Abbreviation_Test.thy b/lib/test/Match_Abbreviation_Test.thy
index d9462baf7..1e682b137 100644
--- a/lib/test/Match_Abbreviation_Test.thy
+++ b/lib/test/Match_Abbreviation_Test.thy
@@ -7,7 +7,7 @@ theory Match_Abbreviation_Test
 
 imports
   Lib.Match_Abbreviation
-  Lib.NonDetMonad
+  Monads.NonDetMonad
 begin
 
 experiment
diff --git a/lib/test/Time_Methods_Cmd_Test.thy b/lib/test/Time_Methods_Cmd_Test.thy
index b4efee3bb..8803fa578 100644
--- a/lib/test/Time_Methods_Cmd_Test.thy
+++ b/lib/test/Time_Methods_Cmd_Test.thy
@@ -6,7 +6,7 @@
 
 theory Time_Methods_Cmd_Test imports
   Lib.Time_Methods_Cmd
-  Lib.Eisbach_Methods
+  Eisbach_Tools.Eisbach_Methods
   "HOL-Library.Sublist"
 begin
 
diff --git a/lib/test/Trace_Schematic_Insts_Test.thy b/lib/test/Trace_Schematic_Insts_Test.thy
index 076c99174..e4e1e3d0a 100644
--- a/lib/test/Trace_Schematic_Insts_Test.thy
+++ b/lib/test/Trace_Schematic_Insts_Test.thy
@@ -6,7 +6,7 @@
 
 theory Trace_Schematic_Insts_Test
 imports
-  Lib.Trace_Schematic_Insts
+  Eisbach_Tools.Trace_Schematic_Insts
 begin
 
 text \<open>