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