diff --git a/thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy b/thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy
--- a/thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy
+++ b/thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy
@@ -1,35 +1,35 @@
 theory Lorenz_C1
   imports
     Lorenz_Approximation.Lorenz_Approximation
 begin
 
 locale check_lines_c1 =
   assumes check_lines_c1: "check_lines True ordered_lines"
 begin
 
 lemma all_coarse_results: "Ball (set coarse_results) correct_res" if NF
   apply (rule Ball_coarseI)
    apply fact
    apply (rule check_lines_c1)
   apply eval
   done
 
 theorem lorenz_bounds:
   "\<forall>x \<in> N - \<Gamma>. x returns_to \<Sigma>"                              \<comment> \<open>\<open>R\<close> is well defined\<close>
   "R ` (N - \<Gamma>) \<subseteq> N"                                         \<comment> \<open>\<open>R\<close> is forward invariant\<close>
   "\<forall>x \<in> N - \<Gamma>. (R has_derivative DR x) (at x within \<Sigma>\<^sub>l\<^sub>e)" \<comment> \<open>\<open>DR\<close> is derivative\<close>
   "\<forall>x \<in> N - \<Gamma>. DR x ` \<CC> x \<subseteq> \<CC> (R x)"                        \<comment> \<open>\<open>\<CC>\<close> is mapped strictly into itself\<close>
   "\<forall>x \<in> N - \<Gamma>. \<forall>c \<in> \<CC> x. norm (DR x c) \<ge> \<E> x      * norm c" \<comment> \<open>expansion\<close>
   "\<forall>x \<in> N - \<Gamma>. \<forall>c \<in> \<CC> x. norm (DR x c) \<ge> \<E>\<^sub>p (R x) * norm c"\<comment> \<open>pre-expansion\<close>
   if NF
   using lorenz_bounds_lemma_asym[OF \<open>NF\<close> reduce_lorenz_symmetry, OF all_coarse_results[OF \<open>NF\<close>]]
   by auto
 
 end
 
 interpretation check_lines_c1
   apply unfold_locales
-  oops\<comment> \<open>very very slow: about 50 CPU hours\<close>
-    \<comment> \<open>\<open>by (parallel_check (* "output_c1/lorenz_c1_" *) _ 60 20)\<close>\<close>
+  by (parallel_check (* "output_c1/lorenz_c1_" *) _ 60 20)
+    \<comment> \<open>very very slow: about 50 CPU hours\<close>
 
 end
diff --git a/thys/Ordinary_Differential_Equations/ROOT b/thys/Ordinary_Differential_Equations/ROOT
--- a/thys/Ordinary_Differential_Equations/ROOT
+++ b/thys/Ordinary_Differential_Equations/ROOT
@@ -1,57 +1,57 @@
 chapter AFP
 
 session "Ordinary_Differential_Equations" = "HOL-Analysis" +
   options [timeout = 1200]
   sessions
     "HOL-Decision_Procs"
     Triangle
     "List-Index"
     Affine_Arithmetic
   directories
     "Library"
     "IVP"
   theories
     ODE_Analysis
   document_files
     "root.bib"
     "root.tex"
 
 session "HOL-ODE-Numerics" in "Numerics" = Ordinary_Differential_Equations +
   options [timeout = 10800]
   sessions
     Collections
     Show
     Affine_Arithmetic
     Deriving
     "HOL-Types_To_Sets"
   directories
     "../Refinement"
   theories
     ODE_Numerics
 
 session "Lorenz_Approximation" in "Ex/Lorenz" = "HOL-ODE-Numerics" +
   options [timeout = 1200]
   theories
     Lorenz_Approximation
 
 session "HOL-ODE-Examples" (large) in "Ex" = "HOL-ODE-Numerics" +
   options [timeout = 7200, document = false]
   theories
     ODE_Examples
   document_files (in "../document")
     "root.bib"
 
 session "HOL-ODE-ARCH-COMP" in "Ex/ARCH_COMP" = "HOL-ODE-Numerics" +
   options [timeout = 7200]
   theories
     "Examples_ARCH_COMP"
 
 session "Lorenz_C0" (large) in "Ex/Lorenz/C0" = "Lorenz_Approximation" +
   options [timeout = 14400]
   theories
     Lorenz_C0
 
-session "Lorenz_C1" (large) in "Ex/Lorenz/C1" = "Lorenz_Approximation" +
-  options [timeout = 300 (*360000*)]
+session "Lorenz_C1" (slow very_slow) in "Ex/Lorenz/C1" = "Lorenz_Approximation" +
+  options [timeout = 360000]
   theories
     Lorenz_C1