# HG changeset patch
# User paulson
# Date 1691344806 -3600
# Node ID 1425a366fe7f42f43dd59251498f005561f58677
# Parent  b2bb63d11adedcf95b23e125ae7d9cc4acfc2c8d# Parent  b22f39c54e8cd4e80c92b4dd7982201f9ea26401
merged

diff -r b22f39c54e8c -r 1425a366fe7f README_REPOSITORY
--- a/README_REPOSITORY	Sun Aug 06 18:29:09 2023 +0100
+++ b/README_REPOSITORY	Sun Aug 06 19:00:06 2023 +0100
@@ -45,6 +45,21 @@
 
     isabelle/bin/isabelle doc system
 
+6. Find historical evidence about good or bad behaviour
+   (e.g. in Isabelle/jEdit):
+
+    cd isabelle
+    hg bisect --reset
+    Admin/init -R   #alternative: "hg up -r REV"
+
+    Admin/init && bin/isabelle jedit
+    hg bisect --good
+
+    Admin/init && bin/isabelle jedit
+    hg bisect --bad
+
+    ...
+
 
 Introduction
 ------------
diff -r b22f39c54e8c -r 1425a366fe7f src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Aug 06 18:29:09 2023 +0100
+++ b/src/HOL/ROOT	Sun Aug 06 19:00:06 2023 +0100
@@ -98,7 +98,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [timeout=1800, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"
@@ -111,7 +111,7 @@
     "root.bib"
 
 session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
-  options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   theories
     Complex_Analysis
@@ -125,7 +125,7 @@
     Metric_Arith_Examples
 
 session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
-  options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Algebra"
@@ -322,7 +322,6 @@
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   "
-  options [timeout = 300]
   sessions
     "HOL-Algebra"
   theories
@@ -847,7 +846,6 @@
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
-  options [timeout = 600]
   sessions
     "HOL-Combinatorics"
   theories