Quelle  ROOT

chapter AFP

session Transport = "HOL" +
  description
    "Transport via partial Galois connections and equivalences and basic libraries on top of HOL axioms."
  options
    [timeout = 600]
  sessions
    "HOL-Algebra"
    "HOL-Library"
    "ML_Unification"
  directories
    "HOL_Basics"
    "HOL_Basics/Binary_Relations"
    "HOL_Basics/Binary_Relations/Functions"
    "HOL_Basics/Binary_Relations/Order"
    "HOL_Basics/Binary_Relations/Properties"
    "HOL_Basics/Binary_Relations/Wellfounded_Recursion"
    "HOL_Basics/Functions"
    "HOL_Basics/Functions/Properties"
    "HOL_Basics/HOL_Alignments"
    "HOL_Basics/HOL_Syntax_Bundles"
    "HOL_Basics/Orders"
    "HOL_Basics/Orders/Functions"
    "HOL_Basics/Orders/Functors"
    "HOL_Basics/Predicates"
    "HOL_Basics/Galois"
    "Transport"
    "Transport/Black_Box"
    "Transport/Black_Box/Compositions"
    "Transport/Black_Box/Compositions/Agree"
    "Transport/Black_Box/Compositions/Generic"
    "Transport/Black_Box/Functions"
    "Transport/Black_Box/Natural_Functors"
    "Transport/Examples"
    "Transport/Examples/Prototype"
    "Transport/Examples/Typedef"
    "Transport/White_Box"
  theories
    HOL_Basics
    HOL_Alignments
    HOL_Algebra_Alignments
    HOL_Syntax_Bundles
    Transport_Black_Box
    Transport_White_Box
    Transport
    (*Examples*)
    Transport_Dep_Fun_Rel_Examples
    Transport_Lists_Sets_Examples
    Transport_Partial_Quotient_Types
    Transport_Typedef
    (*Paper*)
    Transport_Via_Partial_Galois_Connections_Equivalences_Paper
  document_files
    "root.tex"
    "root.bib"