src/HOL/ROOT

   description {*
     HOL-Main with explicit proof terms.
   *}
   options [document = false, theory_qualifier = "HOL",
     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
-  sessions "HOL-Library"
+  sessions
+    "HOL-Library"
   theories
     GCD
     Binomial
     "HOL-Library.Old_Datatype"
   files

     Old_SMT
     Refute
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories
     Analysis
   document_files
     "root.tex"
 

   theories
     Approximations
     Circle_Area
 
 session "HOL-Computational_Algebra" in "Computational_Algebra" = HOL +
+  sessions
+    "HOL-Library"
   theories
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
     Field_as_Ring
     Polynomial_Factorial

 
     The theorem says, that every continous linearform, defined on arbitrary
     subspaces (not only one-dimensional subspaces), can be extended to a
     continous linearform on the whole vectorspace.
   *}
-  theories Hahn_Banach
+  sessions
+    "HOL-Library"
+  theories
+    Hahn_Banach
   document_files "root.bib" "root.tex"
 
 session "HOL-Induct" in Induct = HOL +
   description {*
     Examples of (Co)Inductive Definitions.

     http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
 
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
   *}
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Old_Datatype"
   theories [quick_and_dirty]
     Common_Patterns
   theories

 session "HOL-Number_Theory" (timing) in Number_Theory = HOL +
   description {*
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   *}
+  sessions
+    "HOL-Library"
+    "HOL-Algebra"
+    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/FuncSet"
     "~~/src/HOL/Library/Multiset"
     "~~/src/HOL/Algebra/Ring"
     "~~/src/HOL/Algebra/FiniteProduct"

   theories Hoare_Parallel
   document_files "root.bib" "root.tex"
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, browser_info = false]
+  sessions
+    "HOL-Computational_Algebra"
+    "HOL-Number_Theory"
   theories
     Generate
     Generate_Binary_Nat
     Generate_Target_Nat
     Generate_Efficient_Datastructures

   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
     The Isabelle Algebraic Library.
   *}
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories [document = false]
     (* Preliminaries from set and number theory *)
     "~~/src/HOL/Library/FuncSet"
     "~~/src/HOL/Computational_Algebra/Primes"
     "~~/src/HOL/Library/Permutation"

   theories MainZF Games
   document_files "root.tex"
 
 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   options [print_mode = "iff,no_brackets"]
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Library/LaTeXsugar"
   theories Imperative_HOL_ex

 session "HOL-Decision_Procs" (timing) in Decision_Procs = HOL +
   description {*
     Various decision procedures, typically involving reflection.
   *}
   options [document = false]
-  theories Decision_Procs
+  sessions
+    "HOL-Library"
+    "HOL-Algebra"
+  theories
+    Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   options [document = false]
   theories
     Hilbert_Classical

 session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
   options [parallel_proofs = 0, quick_and_dirty = false]
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Computational_Algebra/Primes"
     "~~/src/HOL/Library/State_Monad"

     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
   options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
-  sessions "HOL-Library"
+  sessions
+    "HOL-Library"
   theories
     Eta
     StrongNorm
     Standardization
     WeakNorm

   description {*
     Formalization of a fragment of Java, together with a corresponding virtual
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
   *}
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/While_Combinator"
   theories
     MicroJava
   document_files

 
 session "HOL-ex" in ex = HOL +
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
+  sessions
+    "HOL-Library"
+    "HOL-Number_Theory"
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
     "~~/src/HOL/Library/FuncSet"
     Eval_Examples

 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {*
     Miscellaneous Isabelle/Isar examples.
   *}
   options [quick_and_dirty]
+  sessions
+    "HOL-Library"
+    "HOL-Computational_Algebra"
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Computational_Algebra/Primes"
   theories
     Knaster_Tarski

 
 session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
   description {*
     Verification of the SET Protocol.
   *}
-  theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
-  theories SET_Protocol
+  sessions
+    "HOL-Library"
+  theories [document = false]
+    "~~/src/HOL/Library/Nat_Bijection"
+  theories
+    SET_Protocol
   document_files "root.tex"
 
 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   description {*
     Two-dimensional matrices and linear programming.

     TPTP_Proof_Reconstruction
   theories
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Permutation"
     "~~/src/HOL/Library/Order_Continuity"
     "~~/src/HOL/Library/Diagonal_Subsequence"

     Nonstandard_Analysis
   document_files "root.tex"
 
 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   options [document = false]
-  theories NSPrimes
+  sessions
+    "HOL-Computational_Algebra"
+  theories
+    NSPrimes
 
 session "HOL-Mirabelle" in Mirabelle = HOL +
   options [document = false]
   theories Mirabelle_Test
 

 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
   options [document = false]
+  sessions
+    "HOL-Library"
   theories
     DList
     Quotient_FSet
     Quotient_Int
     Quotient_Message

     Author:     Franz Regensburger
     Author:     Brian Huffman
 
     HOLCF -- a semantic extension of HOL by the LCF logic.
   *}
+  sessions
+    "HOL-Library"
   theories [document = false]
     "~~/src/HOL/Library/Nat_Bijection"
     "~~/src/HOL/Library/Countable"
   theories
     HOLCF (global)