1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7chapter Lib
8
9session Sep_Algebra (lib) = Word_Lib +
10  sessions
11    "HOL-Eisbach"
12    "HOL-Hoare"
13    Lib
14  directories
15    "ex"
16    "ex/capDL"
17  theories
18    "Generic_Separation_Algebras"
19    "MonadSep"
20    "Sep_Forward"
21    "Sep_Cancel_Example"
22    "Sep_Fold"
23    "Sep_Fold_Cancel"
24    "Sep_Eq"
25    "Sep_Util"
26    "Sep_Heap_Instance"
27    "Sep_MP_Example"
28    "Sep_Provers_Example"
29    "Sep_Select_Example"
30    "Sep_Solve_Example"
31    "ex/Sep_Tactics_Test"
32    "ex/Simple_Separation_Example"
33    "ex/VM_Example"
34    "ex/capDL/Separation_D"
35