# HG changeset patch
# User wenzelm
# Date 1567954145 -7200
# Node ID efd9954882287a6ceaeb5e61a7aaa29bbc420dd5
# Parent  29bb1ebb188f82b92b8d10c7c227257865de1623
declare session directories;

diff -r 29bb1ebb188f -r efd995488228 src/CCL/ROOT
--- a/src/CCL/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/CCL/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -10,6 +10,7 @@
     A computational logic for an untyped functional language with
     evaluation to weak head-normal form.
   "
+  directories "ex"
   sessions
     FOL
   theories
diff -r 29bb1ebb188f -r efd995488228 src/CTT/ROOT
--- a/src/CTT/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/CTT/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -16,6 +16,7 @@
     Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
     1991)
   "
+  directories "ex"
   options [thy_output_source]
   theories
     CTT
diff -r 29bb1ebb188f -r efd995488228 src/Doc/ROOT
--- a/src/Doc/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/Doc/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -404,6 +404,8 @@
     "root.tex"
 
 session Tutorial (doc) in "Tutorial" = HOL +
+  directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
+    "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
   options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   theories [threads = 1]
     "ToyList/ToyList_Test"
diff -r 29bb1ebb188f -r efd995488228 src/FOL/ROOT
--- a/src/FOL/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/FOL/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -24,6 +24,7 @@
   description "
     Examples for First-Order Logic.
   "
+  directories "Locale_Test"
   theories
     Natural_Numbers
     Intro
@@ -42,4 +43,3 @@
   theories [document = false, skip_proofs = false]
     "Locale_Test/Locale_Test"
   document_files "root.tex"
-
diff -r 29bb1ebb188f -r efd995488228 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/HOL/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -4,6 +4,7 @@
   description "
     Classical Higher-order Logic.
   "
+  directories "../Tools"
   options [strict_facts]
   theories [dump_checkpoint]
     Main (global)
@@ -349,6 +350,7 @@
   description "
     A new approach to verifying authentication protocols.
   "
+  directories "Smartcard" "Guard"
   theories
     Auth_Shared
     Auth_Public
@@ -364,6 +366,7 @@
 
     Verifying security protocols using Chandy and Misra's UNITY formalism.
   "
+  directories "Simple" "Comp"
   theories
     (*Basic meta-theory*)
     UNITY_Main
@@ -413,6 +416,7 @@
   document_files "root.tex"
 
 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
+  directories "ex"
   options [print_mode = "iff,no_brackets"]
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
@@ -421,6 +425,7 @@
   description "
     Various decision procedures, typically involving reflection.
   "
+  directories "ex"
   theories
     Decision_Procs
 
@@ -485,6 +490,7 @@
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
   "
+  directories "BV" "Comp" "DFA" "J" "JVM"
   sessions
     "HOL-Eisbach"
   theories
@@ -700,6 +706,7 @@
   description "
     Two-dimensional matrices and linear programming.
   "
+  directories "Compute_Oracle"
   theories Cplex
   document_files "root.tex"
 
@@ -791,6 +798,7 @@
   description "
     (Co)datatype Examples.
   "
+  directories "Derivation_Trees"
   theories
     Compat
     Lambda_Term
@@ -811,6 +819,7 @@
   description "
     Corecursion Examples.
   "
+  directories "Tests"
   theories
     LFilter
     Paper_Examples
@@ -874,6 +883,7 @@
     SPARK
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
+  directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
   theories
     "Gcd/Greatest_Common_Divisor"
     "Liseq/Longest_Increasing_Subsequence"
@@ -968,6 +978,7 @@
   description "
     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   "
+  directories "Examples"
   theories
     Types_To_Sets
     "Examples/Prerequisites"
diff -r 29bb1ebb188f -r efd995488228 src/LCF/ROOT
--- a/src/LCF/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/LCF/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -10,6 +10,7 @@
     Useful references on LCF: Lawrence C. Paulson,
     Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
   "
+  directories "ex"
   sessions
     FOL
   theories
diff -r 29bb1ebb188f -r efd995488228 src/Sequents/ROOT
--- a/src/Sequents/ROOT	Sun Sep 08 13:07:03 2019 +0200
+++ b/src/Sequents/ROOT	Sun Sep 08 16:49:05 2019 +0200
@@ -37,6 +37,7 @@
     S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
     of Cambridge Computer Lab, 1995, ed L. Paulson)
   "
+  directories "LK"
   theories
     LK
     ILL