(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

chapter Lib

session Sep_Algebra (lib) = Word_Lib +
  sessions
    "HOL-Eisbach"
    "HOL-Hoare"
    Lib
  directories
    "ex"
    "ex/capDL"
  theories
    "Generic_Separation_Algebras"
    "MonadSep"
    "Sep_Forward"
    "Sep_Cancel_Example"
    "Sep_Fold"
    "Sep_Fold_Cancel"
    "Sep_Eq"
    "Sep_Util"
    "Sep_Heap_Instance"
    "Sep_MP_Example"
    "Sep_Provers_Example"
    "Sep_Select_Example"
    "Sep_Solve_Example"
    "ex/Sep_Tactics_Test"
    "ex/Simple_Separation_Example"
    "ex/VM_Example"
    "ex/capDL/Separation_D"