session "HOL-Lib" in "~~/src/HOL/Library" = HOL +
  description {* Theories that are not part of HOL but used by IsaFoR *}
  options [document = false,checkpoint]
  theories
    AList
    Bit
    Cardinality
    Char_ord
    Code_Char
    Code_Target_Numeral
    DAList
    DAList_Multiset
    Dlist
    Infinite_Set
    IArray
    Finite_Map
    Fraction_Field
    Fundamental_Theorem_Algebra
    Lattice_Syntax
    List_lexord
    Mapping
    Monad_Syntax
    Multiset
    Omega_Words_Fun
    theories [checkpoint]
    Option_ord
    Permutation
    Permutations
    Phantom_Type
    Polynomial_Factorial
    Product_Lexorder
    Ramsey
    RBT_Impl
    RBT_Mapping
    Simps_Case_Conv
    While_Combinator
    "~~/src/HOL/Algebra/Ring"
    "~~/src/HOL/Algebra/Module"
    "~~/src/HOL/Algebra/Divisibility"
    "~~/src/HOL/Eisbach/Eisbach"
    "~~/src/HOL/ex/Quicksort"
    "~~/src/HOL/Analysis/Determinants"
    "~~/src/HOL/Number_Theory/Residues"
    "~~/src/HOL/Cardinals/Order_Union"
    theories [checkpoint]
    "~~/src/HOL/Cardinals/Wellorder_Extension"
    "~~/src/HOL/Analysis/Euclidean_Space"
    "~~/src/HOL/Analysis/Brouwer_Fixpoint"
    "~~/src/HOL/Word/Word"
    "~~/src/HOL/Types_To_Sets/Types_To_Sets"

session "HOL-AFP" =  "HOL-Lib" +
  description {* Theories from the Archive of Formal Proofs that are used by IsaFoR *}
  options [document = false,checkpoint]
  theories
    "$AFP/Abstract-Rewriting/Seq"
    "$AFP/Abstract-Rewriting/Abstract_Rewriting"
    "$AFP/Abstract-Rewriting/SN_Orders"
    "$AFP/Abstract-Rewriting/SN_Order_Carrier"
    "$AFP/Abstract-Rewriting/Relative_Rewriting"
    "$AFP/Algebraic_Numbers/Complex_Algebraic_Numbers"
    "$AFP/Algebraic_Numbers/Show_Real_Approx"
    "$AFP/Certification_Monads/Check_Monad"
    "$AFP/Collections/Refine_Dflt"
    "$AFP/Containers/Containers"
    "$AFP/Containers/Compatibility_Containers_Regular_Sets"
    "$AFP/Deriving/Comparator_Generator/Compare_Order_Instances"
    "$AFP/Deriving/Comparator_Generator/RBT_Compare_Order_Impl"
    "$AFP/Deriving/Comparator_Generator/RBT_Comparator_Impl"
    "$AFP/Deriving/Derive"
    "$AFP/Decreasing-Diagrams-II/Decreasing_Diagrams_II"
    "$AFP/Echelon_Form/Cayley_Hamilton_Compatible"
    "$AFP/Efficient-Mergesort/Efficient_Sort"
    "$AFP/Gabow_SCC/Gabow_SCC_Code"
    "$AFP/Gauss_Jordan/IArray_Haskell"
    "$AFP/Gauss_Jordan/Elementary_Operations"
    "$AFP/Jordan_Normal_Form/Matrix_Complexity"
    "$AFP/Jordan_Normal_Form/Jordan_Normal_Form_Existence"
    "$AFP/Jordan_Normal_Form/Jordan_Normal_Form_Uniqueness"
    "$AFP/Jordan_Normal_Form/Matrix_Impl"
    "$AFP/Partial_Function_MR/Partial_Function_MR"
    "$AFP/Perron_Frobenius/Spectral_Radius_Theory"
    "$AFP/Polynomials/Polynomials"
    "$AFP/Regular-Sets/Regexp_Method"
    "$AFP/Show/Show_Instances"
    "$AFP/Show/Show_Complex"
    "$AFP/Transitive-Closure/Transitive_Closure_List_Impl"
    "$AFP/Transitive-Closure/Transitive_Closure_RBT_Impl"
    "$AFP/Transitive-Closure/RBT_Map_Set_Extension"
    "$AFP/Transitive-Closure-II/RTrancl"
    "$AFP/VectorSpace/VectorSpace"
    "$AFP/Well_Quasi_Orders/Kruskal"
    "$AFP/XML/Xmlt"

session QTRS = "HOL-AFP" +
  options [document = false,checkpoint]
  theories "Framework/QDP_Framework_Impl"
  theories [checkpoint]

session TA = QTRS +
  options [document = false,checkpoint]
  theories
     "Tree_Automata/Exact_Tree_Automata_Completion_Impl"
     theories [checkpoint]
     "LTS/Simplex/Simplex"

session "Check-NT" = TA +
  options [document = false,checkpoint]
  theories "Nontermination/Nontermination_Processors"
  theories [checkpoint]

session Processors = "Check-NT" +
  options [document = false,checkpoint]
  theories
    "Termination_and_Complexity/Processors"
    theories [checkpoint]

session "Check-Termination" = Processors +
  options [document = false,checkpoint]
  theories
    "Proof_Checker/Check_Termination"
    theories [checkpoint]

session "Proof-Checker" = "Check-Termination" +
  options [document = false]
  theories "Proof_Checker/Proof_Checker"
  theories [checkpoint]

session CeTA = "Proof-Checker" +
  options [document = false,checkpoint]
  theories "Proof_Checker/Ceta"


session "CeTA-TermFun" (termfun) in "TermFun" = CeTA +
  options [document = false,checkpoint]
  theories TermFun

session "CeTA-TermFun-Examples" (termfun) in "TermFun/Examples" = "CeTA-TermFun" +
  options [document = false,checkpoint]
  theories
    Loga
    Examples
    theories [checkpoint]
    Gcd
    Regression
    Bin_Tree
    theories [checkpoint]
    Mktree
    Nnf
    Sum
    HO

session "CeTA-Fast" = "HOL-AFP" +
  description {* Just run dependencies without building intermediate heap images. *}
  options [document = false,checkpoint]
  theories
    "Proof_Checker/Ceta"

session "Code" (ceta) = "CeTA" +
  options [document = false,checkpoint]
  theories
    "Proof_Checker/Code_Haskell"

session Norm_Equiv (isafor) = QTRS +
  description {* Normalization equivalence. *}
  options [document = false,checkpoint]
  theories
    "Normalization_Equivalence/Normalization_Equivalence"

session PCP (isafor) = QTRS +
  description {* Abstact completion with prime critical pairs. *}
  options [document = false,checkpoint]
  theories
    "Abstract_Completion/Completion_Fairness"


session AC (isafor) = "HOL-AFP" +
  description {* Rewriting modulo Associativity and Commutativity *}
  options [document = false,checkpoint]
  theories
    "AC_Rewriting/AC_Equivalence"

session CCR = Processors +
  description {* Bundles all theories immediately before conditional CR check. *}
  options [document = false,checkpoint]
  theories
    "Proof_Checker/Check_CRP"
    theories [checkpoint]
    "Proof_Checker/Check_Quasi_Reductive"
    theories [checkpoint]
    "Conditional_Rewriting/AL94_Impl"
    theories [checkpoint]
    "Conditional_Rewriting/Non_Confluence2"
    theories [checkpoint]