diff --git a/thys/BTree/ROOT b/thys/BTree/ROOT
--- a/thys/BTree/ROOT
+++ b/thys/BTree/ROOT
@@ -1,35 +1,35 @@
 chapter AFP
 
 session "BTree" (AFP) = "Refine_Imperative_HOL" +
-  options [timeout = 1200]
+  options [timeout = 2400]
   sessions
     "HOL-Data_Structures"
     "HOL-Real_Asymp"
   theories
     BTree
     BTree_Height
     BTree_Set
     BTree_Split
     BPlusTree
     BPlusTree_Split
     BPlusTree_Set
     BPlusTree_Range
     BPlusTree_SplitCE
   theories [condition = ISABELLE_OCAMLFIND]
     Array_SBlit
     Partially_Filled_Array
     BTree_Imp
     BTree_ImpSet
     BTree_ImpSplit
     Flatten_Iter_Spec
     Flatten_Iter
     BPlusTree_Imp
     BPlusTree_ImpSplit
     BPlusTree_ImpSet
     BPlusTree_Iter_OneWay
     BPlusTree_Iter
     BPlusTree_ImpRange
     BPlusTree_ImpSplitCE
   document_files
     "root.tex"
     "root.bib"
diff --git a/thys/CZH_Elementary_Categories/ROOT b/thys/CZH_Elementary_Categories/ROOT
--- a/thys/CZH_Elementary_Categories/ROOT
+++ b/thys/CZH_Elementary_Categories/ROOT
@@ -1,15 +1,15 @@
 chapter AFP
 
 session CZH_Elementary_Categories (AFP) = CZH_Foundations +
-  options [timeout = 7200]
+  options [timeout = 3600]
   directories
     czh_ecategories
   theories
     CZH_ECAT_Conclusions
   document_files
     "iman.sty"
     "extra.sty"
     "isar.sty"
     "style.sty"
     "root.tex"
     "root.bib"
\ No newline at end of file
diff --git a/thys/Category3/ROOT b/thys/Category3/ROOT
--- a/thys/Category3/ROOT
+++ b/thys/Category3/ROOT
@@ -1,11 +1,11 @@
 chapter AFP
 
 session "Category3" (AFP) = "HOL-Library" +
-  options [timeout = 3000, names_unique = false]
+  options [timeout = 3600, names_unique = false]
   sessions
     "HereditarilyFinite" "ZFC_in_HOL"
   theories
     EquivalenceOfCategories HFSetCat ZFC_SetCat
   document_files
     "root.bib"
     "root.tex"
diff --git a/thys/Complex_Bounded_Operators/ROOT b/thys/Complex_Bounded_Operators/ROOT
--- a/thys/Complex_Bounded_Operators/ROOT
+++ b/thys/Complex_Bounded_Operators/ROOT
@@ -1,19 +1,19 @@
 chapter AFP
 
 session Complex_Bounded_Operators(AFP) = "HOL-Analysis" +
-  options [timeout = 2400]
+  options [timeout = 3600]
   sessions
     "HOL-Examples"
     "HOL-Types_To_Sets"
     Jordan_Normal_Form
     Banach_Steinhaus
     Real_Impl
   directories
     extra
   theories
     Complex_L2
     Cblinfun_Code
     Cblinfun_Code_Examples
   document_files
     root.tex
     root.bib
diff --git a/thys/FSM_Tests/ROOT b/thys/FSM_Tests/ROOT
--- a/thys/FSM_Tests/ROOT
+++ b/thys/FSM_Tests/ROOT
@@ -1,65 +1,65 @@
 chapter AFP
 
 session FSM_Tests (AFP) = "HOL-Library" + 
-  options [timeout = 600]
+  options [timeout = 2400]
   sessions
     "Datatype_Order_Generator"
     "Containers"
     "Native_Word"
   directories
     "AdaptiveStateCounting"
     "EquivalenceTesting"
   theories
     "Util"
     "Util_Refined"
     "FSM_Impl"
     "FSM"
     "Product_FSM"
     "Distinguishability"
     "IO_Sequence_Set"
     "Minimisation"
     "Observability"
     "Prefix_Tree"
     "Prefix_Tree_Refined"
     "Prime_Transformation"
     "State_Cover"
     "OFSM_Tables_Refined"
     
     "EquivalenceTesting/Convergence"
     "EquivalenceTesting/Convergence_Graph"
     "EquivalenceTesting/Empty_Convergence_Graph"
     "EquivalenceTesting/H_Framework"
     "EquivalenceTesting/H_Method_Implementations"    
     "EquivalenceTesting/HSI_Method_Implementations"
     "EquivalenceTesting/Intermediate_Frameworks"
     "EquivalenceTesting/Intermediate_Implementations"
     "EquivalenceTesting/Pair_Framework"
     "EquivalenceTesting/Partial_S_Method_Implementations"
     "EquivalenceTesting/Simple_Convergence_Graph"
     "EquivalenceTesting/SPY_Framework"
     "EquivalenceTesting/SPY_Method_Implementations"    
     "EquivalenceTesting/SPYH_Method_Implementations"
     "EquivalenceTesting/Test_Suite_Representations_Refined"
     "EquivalenceTesting/Test_Suite_Representations"
     "EquivalenceTesting/W_Method_Implementations"
     "EquivalenceTesting/Wp_Method_Implementations"
     
     "AdaptiveStateCounting/Adaptive_Test_Case"
     "AdaptiveStateCounting/Backwards_Reachability_Analysis"
     "AdaptiveStateCounting/Helper_Algorithms"
     "AdaptiveStateCounting/Maximal_Path_Trie"
     "AdaptiveStateCounting/R_Distinguishability"    
     "AdaptiveStateCounting/State_Preamble"
     "AdaptiveStateCounting/State_Separator"
     "AdaptiveStateCounting/Test_Suite_Calculation"
     "AdaptiveStateCounting/Test_Suite_Calculation_Refined"
     "AdaptiveStateCounting/Test_Suite_IO"
     "AdaptiveStateCounting/Test_Suite"
     "AdaptiveStateCounting/Traversal_Set"
 
     "FSM_Code_Datatype"
     "Test_Suite_Generator_Code_Export"
   document_files
     "root.tex"
     "root.bib"
   export_files (in "code_export") [2] "FSM_Tests.Test_Suite_Generator_Code_Export:code**"
\ No newline at end of file
diff --git a/thys/Solidity/ROOT b/thys/Solidity/ROOT
--- a/thys/Solidity/ROOT
+++ b/thys/Solidity/ROOT
@@ -1,27 +1,27 @@
 chapter AFP
 
 session Solidity (AFP) = "HOL-Library" +
-  options [timeout=3000]
+  options [timeout = 7200]
   sessions
     "HOL-Eisbach"
   theories
     ReadShow
     StateMonad
     Valuetypes
     Storage
     Accounts
     Environment
     Statements
     Solidity_Main
     Solidity_Symbex
     Solidity_Evaluator
     Constant_Folding
     Reentrancy
   theories [condition = ISABELLE_GHC]
     Compile_Evaluator
   document_files
     "root.tex"
     "root.bib"
     "orcidlink.sty"
   export_files (in ".") [2] "*:**.hs" "*:**.ML"
   export_files (in "solidity-evaluator/bin") [1] "*:solidity-evaluator"