diff --git a/thys/HOL-CSP/ROOT b/thys/HOL-CSP/ROOT
--- a/thys/HOL-CSP/ROOT
+++ b/thys/HOL-CSP/ROOT
@@ -1,63 +1,63 @@
 chapter AFP
 
 (*****************************************************************************
  *
  * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
  * Version         : 2.0
  *
  * Author          : Burkhart Wolff, Safouan Taha & Lina Ye
  *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
  *
  * This file       : A Combined CSP Theory
  *
  * Copyright (c) 2009 Université Paris-Sud, France
  *
  *
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are
  * met:
  *
  *     * Redistributions of source code must retain the above copyright
  *       notice, this list of conditions and the following disclaimer.
  *
  *     * Redistributions in binary form must reproduce the above
  *       copyright notice, this list of conditions and the following
  *       disclaimer in the documentation and/or other materials provided
  *       with the distribution.
  *
  *     * Neither the name of the copyright holders nor the names of its
  *       contributors may be used to endorse or promote products derived
  *       from this software without specific prior written permission.
  *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
  * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
  * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
  * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
  * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
  * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  ******************************************************************************)
 (* $Id:$ *)
 
 session "HOL-CSP" (AFP) = HOLCF +
   description {* HOL-CSP based on the original Roscoe-Book. *}
-  options [timeout = 600]
+  options [timeout = 1200]
   sessions
     "HOL-Eisbach"
   theories
     "Introduction"
     "Process"
      Bot Skip Stop Mprefix Det Ndet Seq Hide Sync Mndet
     "CSP" "Assertions"
     "Conclusion"
     "CopyBuffer"
   document_files
     "root.tex"
     "adb-long.bib"
     "root.bib"
diff --git a/thys/Modal_Logics_for_NTS/ROOT b/thys/Modal_Logics_for_NTS/ROOT
--- a/thys/Modal_Logics_for_NTS/ROOT
+++ b/thys/Modal_Logics_for_NTS/ROOT
@@ -1,41 +1,41 @@
 chapter AFP
 
 session "Modal_Logics_for_NTS" (AFP) = Nominal2 +
-  options [timeout = 600]
+  options [timeout = 900]
   sessions
     "HOL-Cardinals"
   theories
     (* Strong Bisimilarity *)
     Nominal_Bounded_Set
     Nominal_Wellfounded
     Residual
     Transition_System
     Formula
     Validity
     Logical_Equivalence
     Bisimilarity_Implies_Equivalence
     Equivalence_Implies_Bisimilarity
     Disjunction
     Expressive_Completeness
     (* Generalization to F/L-Bisimilarity *)
     FS_Set
     FL_Transition_System
     FL_Formula
     FL_Validity
     FL_Logical_Equivalence
     FL_Bisimilarity_Implies_Equivalence
     FL_Equivalence_Implies_Bisimilarity
     L_Transform
     (* Weak Bisimilarity *)
     Weak_Transition_System
     Weak_Formula
     Weak_Validity
     Weak_Logical_Equivalence
     Weak_Bisimilarity_Implies_Equivalence
     Weak_Equivalence_Implies_Bisimilarity
     Weak_Expressive_Completeness
     (* State Predicates Versus Actions *)
     S_Transform
   document_files
     "root.bib"
     "root.tex"
diff --git a/thys/Probabilistic_Prime_Tests/ROOT b/thys/Probabilistic_Prime_Tests/ROOT
--- a/thys/Probabilistic_Prime_Tests/ROOT
+++ b/thys/Probabilistic_Prime_Tests/ROOT
@@ -1,14 +1,14 @@
 chapter AFP
 
 session Probabilistic_Prime_Tests (AFP) = "HOL-Probability" +
-  options [timeout = 1200]
+  options [timeout = 1500]
   sessions
     "HOL-Algebra"
     "HOL-Computational_Algebra"
     "HOL-Number_Theory"
   theories
     Fermat_Test
     Miller_Rabin_Test
     Solovay_Strassen_Test
   document_files
     "root.tex"