# HG changeset patch
# User wenzelm
# Date 1491337002 -7200
# Node ID de848ac5e0d72361b9abd59ccd4893604141fe5a
# Parent  9d9e6dac9690e90623bd6098ce2c0c43b9efd0ff
more main sessions and global theories;

diff -r 9d9e6dac9690 -r de848ac5e0d7 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Apr 04 22:07:34 2017 +0200
+++ b/src/HOL/ROOT	Tue Apr 04 22:16:42 2017 +0200
@@ -62,7 +62,7 @@
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
   theories
-    Analysis
+    Analysis (global)
   document_files
     "root.tex"
 
@@ -716,7 +716,7 @@
   theories
     ATP_Problem_Import
 
-session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" +
+session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Permutation"
@@ -724,7 +724,7 @@
     "~~/src/HOL/Library/Diagonal_Subsequence"
     "~~/src/HOL/Library/Finite_Map"
   theories
-    Probability
+    Probability (global)
   document_files "root.tex"
 
 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
@@ -820,7 +820,8 @@
     "Tests/Type_Class"
 
 session "HOL-Word" (main timing) in Word = HOL +
-  theories Word
+  theories
+    Word (global)
   document_files "root.bib" "root.tex"
 
 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
@@ -868,7 +869,8 @@
 
 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   options [document = false]
-  theories SPARK
+  theories
+    SPARK (global)
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   options [document = false, spark_prv = false]
@@ -1035,7 +1037,7 @@
     "~~/src/HOL/Library/Nat_Bijection"
     "~~/src/HOL/Library/Countable"
   theories
-    HOLCF
+    HOLCF (global)
   document_files "root.tex"
 
 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +